代码契约[Type]实现接口方法{Interface.Method}，因此无法添加要求

Question

我有以下场景：

public interface ISomething
{
    void DoStuff();
    //...
}

public class Something : ISomething
{
    private readonly ISomethingElse _somethingElse;
    //...

    public Something (ISomethingElse somethingElse)
    {
         Contract.Requires(somethingElse != null);
        _somethingElse = somethingElse;
    }

    public void DoStuff()
    {
        // *1* Please look at explanation / question below
        _somethingElse.DoThings();
    }
 }

在第 1 行并打开静态检查器时，我会收到一条警告，指出 _somethingElse 可能为空，如果我添加合同会给我错误

[Type]实现接口方法{Interface.Method}，因此无法添加要求

这里最好做什么？我看到的选项包括

1. 一个保护条款，尽管它似乎是 有点极端
2. Contract.Assume
3. 我没有想到的隐藏的第三个选项

请注意，该字段是只读，因此在构造函数中设置值后，不可能改变。因此，代码合约的警告似乎有点无关紧要。

Answer 1

说明

用户手册的第 3 节：合同继承 声明所有前提条件必须在继承/实现链的根方法中定义：

如果客户端确保他们已经满足前提条件并且有一个静态类型为 T 的变量 o，那么当客户端致电oM。即使运行时值 o 的类型为 U，也必须如此。因此，UM 方法无法添加比 TM 的前提条件更强的前提条件。

虽然我们可以允许较弱的前提条件，但我们发现这样做的复杂性超过了好处。我们只是还没有看到任何令人信服的例子来证明弱化前提条件是有用的。因此我们根本不允许在子类型中添加任何先决条件。

因此，方法前置条件必须在继承/实现链的根方法上声明，即第一个虚拟或抽象方法声明，或接口方法本身。

解决方案

在您的情况下，最好的做法是设置一个不变量，声明 _somethingElse 字段永远不为空：

[ContractInvariantMethod]
private void ObjectInvariant() {
    Contract.Invariant(_somethingElse != null);
}

这当然总是正确的，因为该字段被标记为 readonly 并在构造函数中初始化。不过，静态检查器无法自行推断这一点，因此您必须通过该不变量显式地告诉它。

您可以选择向构造函数添加后置条件 Contract.Ensures(_somethingElse != null);，但静态检查器不需要它。