代码合同：确保未经证实和需要未经证实

我不确定我在这里做错了什么，或者是否需要修复......

我有一个自定义的Dictionary封装类，这里是必需的代码片段。

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 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 method'System.Collections.Generic.IDictionary 2.ContainsKey（type parameter.TKey）'，因此无法添加Requires。

---

“我有一个自定义Dictionary封装类” - 它实现了IDictionary<TKey, TValue> 。 接口方法可以指定契约，并且实现它们的类方法必须符合契约。 在这种情况下， IDictionary<TKey, TValue>.ContainsKey(TKey)具有您要求的合同：

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

逻辑上， !a || b !a || b可以理解为a ===> b （ a意味着b ），并且使用它，我们可以把它翻译成英文：

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

这是一个非常明智的要求。 空字典不得声称包含密钥。 这是你需要证明的。

下面是一个示例DictionaryWrapper类，它添加了Contract.Ensures以保证Count的实现细节等于innerDictionary.Count是其他方法可以依赖的一个硬性保证。 它向ContainsKey添加了一个类似的Contract.Ensures ，以便IDictionary<TKey, TValue>.TryGetValue合同也是可验证的。

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

---

坦率地说，我不明白合同的要点。 合同是

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

你想说什么？ 您既不能保证字典中包含密钥，也不能保证字典中包含任何值。 所以这个合同不能总是得到满足。 这就是验证者告诉你的：它不能证明你所承诺的这个陈述是真实的。

您可以确保最好的返回值为true或返回值为false ，并且Count大于零或等于零但是这样的合同有什么意义？ 来电者已经知道这一点。

既然如此，我根本就不打算在这里签合同。

链接地址: http://www.djcxy.com/p/74409.html

上一篇: Code Contracts: Ensures Unproven & Requires Unproven

下一篇: Code Contracts warning about possibly failing 'Assume' call