코드 계약 : 검증되지 않은 보장 및 요구 검증되지 않은

Question

을 내가 잘못 여기거나 수정해야 할 경우 뭔가를하고있어 잘 모르겠어요 ...

내가 정의 사전 래퍼 클래스를 가지고 있으며 여기에 조각입니다 필요한 코드를 나는 다음과 같은 경고 메시지를 받았습니다 (그리고 아직도) 때문에

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

나는 ContainsKey의 라인을 추가하는 유일한 이유는 : Codecontracts: ensures unproven: !Contract.Result<bool>() || @this.Count > 0. 이 행을 삭제해도 여전히 같은 문제가 발생합니다!

이러한 문제를 해결하려면 여기에서 어떻게해야합니까?

---

업데이트 :

나는 또한 (제안) 시도 ...

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

    return InternalDictionary.ContainsKey(key); 
} 

경고 5 방법 'My.Collections.Generic.ReadOnlyDictionary 2.ContainsKey(type parameter.TKey)' implements interface method 'System.Collections.Generic.IDictionary 2.ContainsKey (유형 매개 변수. 키) '이므로 추가 할 수 없습니다. 필요합니다.

Answer 1

솔직히 나는 계약의 요지를 이해하지 못합니다. 계약은

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

무엇을 말하려고합니까? 사전에 키가 포함되어 있는지 또는 사전에 값이 포함되어 있는지 보장 할 수 없습니다. 따라서이 계약이 항상 충족 될 수는 없습니다. 그것이 검증자가 당신에게 말하는 것입니다 : 당신이 진실이라고 약속 한 진술이 사실임을 증명할 수는 없습니다.

당신이 반환 값이 true 또는 반환 값이 false하고 Count 것을 제로보다 큰 제로 거나 같은이다 그러나 그러한 계약의 포인트가 무엇을 보장 할 수있는 가장 좋은? 발신자는 이미 이것을 알고 있습니다.

이 점을 감안할 때, 여기서는 계약을 전혀 신경 쓰지 않을 것입니다.

Answer 2

"사용자 정의 사전 래퍼 클래스가 있습니다."- IDictionary<TKey, TValue>을 구현합니다. 인터페이스 메서드는 계약을 지정할 수 있으며이를 구현하는 클래스 메서드는 계약을 충족해야합니다. 이 경우, IDictionary<TKey, TValue>.ContainsKey(TKey)가 당신에 대해 요구하고있는 계약이 있습니다 논리적으로

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

을 !a || b 우리가 영어이 번역 할 수 있음 (a가 b을 의미) a ===> b로 읽고, 사용 할 수 있습니다

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

이것은 매우 합리적인 요구 사항입니다. 빈 사전은 키를 포함해서는 안됩니다. 이은 귀하가 증명해야하는 것입니다.

여기에 다른 방법에 의존 할 수있는 하드 보장이 Count의 구현 세부 사항 innerDictionary.Count 동일한 것을 약속하는 Contract.Ensures을 추가하는 샘플 DictionaryWrapper 클래스입니다.IDictionary<TKey, TValue>.TryGetValue 계약을 확인할 수 있도록 ContainsKey에 비슷한 Contract.Ensures을 추가합니다.

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