从IDictionary <T,U>这样的接口派生时如何使用代码契约？

Question

我写的一个课程实现IDictionary<string, object>.在我的CopyTo实现中,我想使用代码契约:像Contract.Requires<ArgumentNullException>(array != null).

但是,我收到此警告(为了便于阅读,删除了一些名称空间):

方法' LuaDictionary.CopyTo(KeyValuePair<String,Object>[],Int32)'实现接口方法' ICollection<KeyValuePair<String,Object>>.CopyTo(KeyValuePair<String,Object>[],Int32)',因此无法添加Requires.

我看到有一些相关的问题,但它们似乎都与用户控制下的接口有关.显然,IDictionary<T, U>不在我的控制之下,所以我不能用它ContractClassFor或类似的东西注释它.

我在这里无法使用代码合同吗？如果是这样......主要的无赖......

Answer 1

这是一个无赖,但是可以理解,因为使用您的类的实例的客户端代码IDictionary<string, object>不应该满足不期望的前提条件IDictionary<string, object>.

您可以阅读提供给此SO问题的答案,该问题链接并引用代码合同用户手册,您可以查看本文,以这种方式解释这种情况,并继续提供一个简单示例:

请注意,Liskov的替换原则适用于代码契约,其方式与普通类完全相同.利斯科夫的原则如下:

子类应始终可替代其基类.

就Code Contracts API而言,这意味着派生类(或实现基于契约的接口的类)不应期望更多的前提条件作为父类.

Answer 2

请记住,IDictionary<K,V>已经有Requires:)

您可以在以下位置查看类的现有合同DLL : C:\Program Files (x86)\Microsoft\Contracts.

如果mscorlib.Contracts.dll使用Reflector 打开,则可以查看集合类的合同; CopyTo有以下内容:

public void CopyTo(T[] array, int arrayIndex)
{
    Contract.Requires((bool)(array != null), null, "array != null");
    Contract.Requires((bool)(arrayIndex >= 0), null, "arrayIndex >= 0");
    Contract.Requires((bool)((arrayIndex + this.Count) <= array.Length), null, "arrayIndex + this.Count  <= array.Length");
}