Code Contracts: Asegura no probados y no probados Requiere

Question

No estoy seguro de si estoy haciendo algo mal aquí o si necesita ser arreglado ...

que tienen una clase contenedora personalizada diccionario y aquí es un fragmento del código que es necesario.

public int Count 
{ 
    get 
    { 
     Contract.Ensures(Contract.Result<int>() >= 0); 

     return InternalDictionary.Count; 
    } 
} 

public bool ContainsKey(TKey key) 
{ 
    //This contract was suggested by the warning message, if I remove it 
    //I still get the same warning... 
    Contract.Ensures(!Contract.Result<bool>() || Count > 0); 

    return InternalDictionary.ContainsKey(key); 
} 

La única razón por la que añadí la línea para el ContainsKey es porque me dieron el siguiente mensaje de advertencia (y todavía lo hacen): Codecontracts: ensures unproven: !Contract.Result<bool>() || @this.Count > 0. Me puede quitar esta línea y aún obtener el mismo problema !

¿qué es lo que hago aquí para deshacerse de estos problemas?

---

Actualización:

También probé (como se sugiere) ...

public Boolean ContainsKey(TKey key) 
{ 
    Contract.Requires(Count == 0 || InternalDictionary.ContainsKey(key)); 
    Contract.Ensures(!Contract.Result<bool>() || Count > 0); 

    return InternalDictionary.ContainsKey(key); 
} 

Advertencia 5 Método 'My.Collections.Generic.ReadOnlyDictionary 2.ContainsKey(type parameter.TKey)' implements interface method 'System.Collections.Generic.IDictionary 2.ContainsKey (tipo parameter.TKey) ', por lo tanto no puede agregar Requiere.

Answer 1

Francamente no entiendo el punto del contrato. El contrato es

Contract.Ensures(!Contract.Result<bool>() || Count > 0); 

¿Qué estás tratando de decir? No puede garantizar que el diccionario contenga la clave ni que el diccionario contenga ningún valor. Entonces este contrato no siempre se puede cumplir. Eso es lo que el verificador te está diciendo: no puede probar que esta afirmación que prometes ser verdadera sea verdadera.

Lo mejor que puede asegurarse de que el valor de retorno es true o el valor de retorno es false y que Count es mayor que cero o igual a cero Pero cuál es el punto de un contrato de este tipo? La persona que llama ya sabe esto.

Teniendo en cuenta que, no me molestaría con un contrato aquí en absoluto.

Answer 2

"Tengo una clase contenedora personalizada Diccionario" - que implementa IDictionary<TKey, TValue>. Los métodos de interfaz pueden especificar contratos, y los métodos de clase que los implementan deben cumplir los contratos. En este caso, IDictionary<TKey, TValue>.ContainsKey(TKey) tiene el contrato que estés preguntando por:

Contract.Ensures(!Contract.Result<bool>() || this.Count > 0); 

Lógicamente, !a || b puede leerse como a ===> b (a implica b), y el uso que podemos traducir esto a Inglés:

If ContainsKey() returns true, the dictionary must not be empty. 

Este es un requisito perfectamente razonable. Un diccionario vacío no debe pretender contener claves. Esto es lo que necesita probar.

Aquí es una clase de muestra DictionaryWrapper que añade Contract.Ensures prometer que el detalle de implementación de Count igual a innerDictionary.Count es una garantía dura que otros métodos pueden confiar.Agrega un Contract.Ensures similar a ContainsKey para que el contrato IDictionary<TKey, TValue>.TryGetValue también sea verificable.

public class DictionaryWrapper<TKey, TValue> : IDictionary<TKey, TValue> 
{ 
    IDictionary<TKey, TValue> innerDictionary; 

    public DictionaryWrapper(IDictionary<TKey, TValue> innerDictionary) 
    { 
     Contract.Requires<ArgumentNullException>(innerDictionary != null); 
     this.innerDictionary = innerDictionary; 
    } 

    [ContractInvariantMethod] 
    private void Invariant() 
    { 
     Contract.Invariant(innerDictionary != null); 
    } 

    public void Add(TKey key, TValue value) 
    { 
     innerDictionary.Add(key, value); 
    } 

    public bool ContainsKey(TKey key) 
    { 
     Contract.Ensures(Contract.Result<bool>() == innerDictionary.ContainsKey(key)); 
     return innerDictionary.ContainsKey(key); 
    } 

    public ICollection<TKey> Keys 
    { 
     get 
     { 
      return innerDictionary.Keys; 
     } 
    } 

    public bool Remove(TKey key) 
    { 
     return innerDictionary.Remove(key); 
    } 

    public bool TryGetValue(TKey key, out TValue value) 
    { 
     return innerDictionary.TryGetValue(key, out value); 
    } 

    public ICollection<TValue> Values 
    { 
     get 
     { 
      return innerDictionary.Values; 
     } 
    } 

    public TValue this[TKey key] 
    { 
     get 
     { 
      return innerDictionary[key]; 
     } 
     set 
     { 
      innerDictionary[key] = value; 
     } 
    } 

    public void Add(KeyValuePair<TKey, TValue> item) 
    { 
     innerDictionary.Add(item); 
    } 

    public void Clear() 
    { 
     innerDictionary.Clear(); 
    } 

    public bool Contains(KeyValuePair<TKey, TValue> item) 
    { 
     return innerDictionary.Contains(item); 
    } 

    public void CopyTo(KeyValuePair<TKey, TValue>[] array, int arrayIndex) 
    { 
     innerDictionary.CopyTo(array, arrayIndex); 
    } 

    public int Count 
    { 
     get 
     { 
      Contract.Ensures(Contract.Result<int>() == innerDictionary.Count); 
      return innerDictionary.Count; 
     } 
    } 

    public bool IsReadOnly 
    { 
     get 
     { 
      return innerDictionary.IsReadOnly; 
     } 
    } 

    public bool Remove(KeyValuePair<TKey, TValue> item) 
    { 
     return innerDictionary.Remove(item); 
    } 

    public IEnumerator<KeyValuePair<TKey, TValue>> GetEnumerator() 
    { 
     return innerDictionary.GetEnumerator(); 
    } 

    IEnumerator IEnumerable.GetEnumerator() 
    { 
     return innerDictionary.GetEnumerator(); 
    } 
}