代码契约：为什么有些不变量不在类之外考虑？

Question

考虑这个不可变类型：

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 字段上），在静态检查期间无法满足（参见上面的评论）。这对我来说听起来有点奇怪，因为很容易证明这一点：

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

我在这里错过了什么吗？

Answer 1

检查代码契约论坛后，我发现这个类似的问题，其中一个答案如下开发商：

我认为您遇到的行为是由正在进行的某些方法间推理引起的。静态检查器首先分析构造函数，然后分析属性，最后分析方法。在分析 Sample 的构造函数时，它不知道 msgContainer.Something != null，因此会发出警告。解决这个问题的一种方法是在构造函数中添加假设 msgContainer.Something != null ，或者更好地将后置条件 != 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

不变量不适用于私有成员，您实际上无法知道为什么会这样，希望这会有所帮助。