Code Contracts 实现接口方法{Interface.Method}因此无法添加需求

我有以下情况：

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可能为null，如果我添加一个合同，它会给我错误

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

这里最好的事情是什么？ 我看到的选项包括

1. 一个保护条款，虽然看起来有点极端
2. Contract.Assume
3. 一个我没想过的隐藏的第三个选项

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

Answer 1

说明

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

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

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

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

解

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

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

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

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