我不确定我是否在这里做错了什么或者是否需要修复...
我有一个自定义的 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
.我可以删除此行并仍然得到 SAME ISSUE!
我该怎么做才能摆脱这些问题?
更新:
我也试过(按照建议)...
public Boolean ContainsKey(TKey key)
{
Contract.Requires(Count == 0 || InternalDictionary.ContainsKey(key));
Contract.Ensures(!Contract.Result<bool>() || Count > 0);
return InternalDictionary.ContainsKey(key);
}
Warning 5 Method 'My.Collections.Generic.ReadOnlyDictionary
2.ContainsKey(type parameter.TKey)' implements interface method 'System.Collections.Generic.IDictionary
2.ContainsKey(type parameter.TKey)', thus cannot add Requires.
最佳答案
“我有一个自定义的字典包装器类”——它实现了 IDictionary<TKey, TValue>
.接口(interface)方法可以指定契约,实现它们的类方法必须满足契约。在这种情况下,IDictionary<TKey, TValue>.ContainsKey(TKey)
有您询问的契约(Contract):
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
的类 promise Count
的实现细节等于innerDictionary.Count
是其他方法可以依赖的硬保证。它添加了一个类似的 Contract.Ensures
至 ContainsKey
这样 IDictionary<TKey, TValue>.TryGetValue
契约(Contract)也是可验证的。
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();
}
}
关于c# - 代码契约(Contract) : Ensures Unproven & Requires Unproven,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/7419134/