Code Contracts [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. 一个我没想过的隐藏的第三个选项

请注意readonly,在构造函数中设置值后,该字段是如此,因此无法更改.因此,代码合同的警告似乎有点无关紧要.

Answer 1

说明

第3部分:合同继承所述的用户手册,所有先决条件必须在一个继承/实现链的根的方法来定义的状态:

如果客户端确保它们满足前提条件并且具有o静态类型的变量T,则客户端在调用时不应该违反前提条件o.M.即使运行时值o具有类型,也必须如此U.因此,该方法U.M不能添加强于前提条件的前提条件T.M.

虽然我们可以允许更弱的前提条件,但我们发现这样做的复杂性超过了益处.我们还没有看到任何令人信服的例子,其中弱化前提条件是有用的.所以我们不允许在子类型中添加任何先决条件.

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

解

在您的情况下,最好的做法是设置一个不变的声明,该_somethingElse字段永远不为null:

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

这当然总是正确的,因为字段readonly在构造函数中被标记和初始化.静态检查器无法自行推断,因此您必须通过该不变量明确告知它.

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