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属性.

现在,看看这个类型：

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.Path不能为空(因为设置具有相应的契约不变量)
>所以通过将settings.Path分配给_path,_path不能为空

我在这里错过了什么吗？