codice dei contratti: Assicura Non dimostrata & Richiede Non dimostrata

Question

Non sono sicuro se sto facendo qualcosa di sbagliato qui o se ha bisogno di essere fissato ...

Ho un dizionario personalizzato classe wrapper e qui è un frammento del codice che è necessario.

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); 
} 

L'unica ragione per cui ho aggiunto la linea per la ContainsKey è perché ho ottenuto il seguente messaggio di avviso (e continuo a farlo): Codecontracts: ensures unproven: !Contract.Result<bool>() || @this.Count > 0. Posso rimuovere questa riga e ottenere ancora lo SAME ISSUE!

Cosa faccio qui per sbarazzarsi di questi problemi?

---

Aggiornamento:

Ho anche provato (come suggerito) ...

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

    return InternalDictionary.ContainsKey(key); 
} 

Attenzione 5 Metodo 'My.Collections.Generic.ReadOnlyDictionary 2.ContainsKey(type parameter.TKey)' implements interface method 'System.Collections.Generic.IDictionary 2.ContainsKey (tipo parameter.TKey) ', quindi non può aggiungere Richiede.

Answer 1

Francamente non capisco il punto del contratto. Il contratto è

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

Che cosa stai cercando di dire? Non è possibile garantire che il dizionario contenga la chiave, né che il dizionario contenga alcun valore. Quindi questo contratto non può essere sempre rispettato. Questo è quello che ti sta dicendo il verificatore: non può dimostrare che questa affermazione che stai promettendo di essere vera è vera.

Il meglio è possibile garantire che il valore di ritorno è true o il valore di ritorno è false e che Count è maggiore di zero o uguale a zero Ma qual è il punto di un tale contratto? Il chiamante lo sa già.

Detto questo, non mi preoccuperei affatto di un contratto.

Answer 2

"Ho un dizionario personalizzato classe wrapper" - che implementa IDictionary<TKey, TValue>. I metodi di interfaccia possono specificare i contratti e i metodi di classe che li implementano devono soddisfare i contratti. In questo caso, IDictionary<TKey, TValue>.ContainsKey(TKey) ha il contratto si sta chiedendo:

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

Logicamente, !a || b può essere letto come a ===> b (a implica b), e l'utilizzo di questo, siamo in grado di tradurre questo a Inglese:

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

Questo è un requisito perfettamente ragionevole. Un dizionario vuoto non deve pretendere di contenere chiavi. Questo è ciò che devi dimostrare.

Ecco un esempio DictionaryWrapper classe che aggiunge Contract.Ensures a promettere che il dettaglio di implementazione di Count essere pari a innerDictionary.Count è una garanzia difficile che altri metodi possono contare su.Aggiunge un simile Contract.Ensures a ContainsKey in modo che anche il contratto IDictionary<TKey, TValue>.TryGetValue sia verificabile.

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(); 
    } 
}