C# 代码契约：如何验证其他程序集中定义的接口方法的参数？

Question

我遇到了一个情况，我不知道该如何解决。 根据用户手册第3节，一个contractmethod，即<在重写方法/属性或接口实现中不允许使用 code>Require 或 Ensure。契约方法应在根虚拟/抽象方法中声明，并且由于您无法在抽象方法中声明代码，因此必须使用 ContractClassAttribute 和 ContractClassForAttribute。接口成员的契约方法（及其实现）也是如此。

但是如果我想使用一个不是我自己创建的界面怎么办？例如，IList 没有实现这些约定方法，但我也无法在其上设置 ContractClassAttribute。我应该如何在 IList.this[int] 的实现中进行参数验证？不允许使用以下解决方案：

T IList<T>.this[int i]
{
    get
    {
        Contract.Requires(i >= 0);//not allowed

        if (i < 0)
            throw new ArgumentException();
        Contract.EndContractBlock();//also not allowed
        ...
    }
}

不带 EndContractBlock 的旧版 if-then-throw 语句是唯一的解决方案吗？

Answer 1

首先，IList已经指定了该前提条件。我只是尝试了一下以确保：“前提条件失败：索引 >= 0”。

此外，据我了解，后置条件是允许的，只有先决条件不允许。

如果您还想添加其他先决条件，我相信这可以回答您的问题：
http://social.msdn.microsoft .com/Forums/en/codecontracts/thread/af403bbc-ca4e-4546-8b7a-3fb3dba4bb4a

这基本上可以归结为这样一个事实：您不应该这样做，因为这会违背代码契约的目的。

Answer 2

不能添加前提条件的原因与不能这样做的原因相同：

interface IInterface
{
    void Foo(Parent x);
}

class Implementation : IInterface
{
    void Foo(Child x);
}

它与（同/反）方差相关 - 方法参数是逆变的，这意味着您接受的类型必须“至少与自由主义”作为接口指定的类型。

添加更多先决条件会使类型更小/更严格，就像接受该类型的子类一样（如上面的示例）。*出于明显的原因，您不能这样做 - 一个实现了当传递正确的参数时，接口可能无法工作！如果你翻转了 Parent & 孩子 没关系。

对于方法返回类型，情况正好相反：它们是协变的，这意味着您必须“至少与接口指定的类型一样小/严格”。这就是为什么您可以添加后置条件，因为您正在使类型“更小/更严格”。这与它起作用的原因相同：

interface IInterface
{
    Parent Foo();
}

class Implementation : IInterface
{
    Child Foo();
}

*（这实际上提出了一个问题：您是否应该能够从实现类中删除前置条件。这将是一个有趣的功能。）