代码合同：为什么有些不变量不在课堂之外考虑？

考虑这种不可变类型：

public class Settings { public string Path { get; private set; } [ContractInvariantMethod] private void ObjectInvariants() { Contract.Invariant(Path != null); } public Settings(string path) { Contract.Requires(path != null); Path = path; } } 

这里要注意两件事：

• 有一个契约不变量，它确保Path属性永远不能为null
• 构造函数检查path参数值以遵守先前的合约不变量

此时， Setting实例永远不能具有null Path属性。

现在，看看这种类型：

 public class Program { private readonly string _path; [ContractInvariantMethod] private void ObjectInvariants() { Contract.Invariant(_path != null); } public Program(Settings settings) { Contract.Requires(settings != null); _path = settings.Path; } // <------ "CodeContracts: invariant unproven: _path != null" } 

基本上，它有自己的契约不变量（在_path字段上），在静态检查期间无法满足（参见上面的注释）。 这对我来说听起来有点奇怪，因为它很容易certificate：

• settings是不可变的
• settings.Path不能为null（因为Settings具有相应的契约不变量）
• 因此，通过将settings.Path分配给_path ， _path不能为null

我在这里错过了什么吗？

Answer 1

在检查代码合同论坛后 ，我发现了一个类似的问题 ，其中一个开发人员给出了以下答案：

我认为您遇到的行为是由正在进行的一些方法间推断引起的。 静态检查器首先分析构造函数，然后分析属性，然后分析方法。 在分析Sample的构造函数时，它不知道msgContainer.Something！= null，因此它会发出警告。 解决它的方法是在构造函数中添加一个假设msgContainer.Something！= null，或者更好地将postcondition！= null添加到Something。

换句话说，您的选择是：

1. 使Settings.Path属性显式而不是自动，并在支持字段上指定不变量。 为了满足你的不变量，你需要为属性的set访问器添加一个前提条件： Contract.Requires(value != null) 。

   您可以选择使用Contract.Ensures(Contract.Result() != null)向get访问器添加后置条件，但静态检查器不会以任何方式进行投诉。

2. 将Contract.Assume(settings.Path != null)到Program类的构造函数中。

Answer 2

不变量不适用于私人成员，你实际上不能有这种方式的原因，希望这有帮助。