代码合同:确保Unpoven&；需要取消烘焙

本文关键字：取消 amp 合同 确保 Unpoven 代码 | 更新日期: 2023-09-27 18:08:30

我不确定我是在这里做错了什么，还是需要修复。。。

我有一个自定义的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。我可以删除这一行，但仍然得到相同的问题！

我该怎么做才能解决这些问题？

更新：

我也试过(按照建议(。。。

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(类型参数.TKey("，因此无法添加需要。

代码合同:确保Unpoven&；需要取消烘焙

"我有一个自定义的Dictionary包装类"-实现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.

这是一个非常合理的要求。空字典不能声称包含关键字这是你需要证明的。

这里有一个示例DictionaryWrapper类，它添加了Contract.Ensures，以保证Count的实现细节等于innerDictionary.Count是其他方法可以依赖的硬保证。它将类似的Contract.Ensures添加到ContainsKey，使得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大于零或等于零但这样的合同有什么意义？打电话的人已经知道了。

考虑到这一点，我根本不会为这里的合同而烦恼。

相关文章：