c# - 代码契约(Contract) : Why are some invariants not considered outside the class?

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不能为null(因为Settings有对应的契约不变量)
• 因此通过将settings.Path赋给_path，_path不能为null

我是不是漏掉了什么？

Answer 1

检查 code contracts forum 后, 我找到了 this similar question其中一位开发人员的回答如下:

I think the behavior you are experiencing is caused by some inter-method inference that is going on. The static checker first analyzes the constructors, then the properties and then the methods. When analyzing the constructor of Sample, it does not know that msgContainer.Something != null so it issues the warning. A way to solve it, is either by adding an assumption msgContainer.Something != null in the constuctor, or better to add the postcondition != null to Something.

换句话说，您的选择是:

1. 制作Settings.Path property explicit 而不是 automatic，并在支持字段上指定不变量。为了满足您的不变量，您需要向属性的 set 访问器添加一个前提条件:Contract.Requires(value != null) .

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

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