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

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不能为空

我在这里错过了什么吗？

Answer 1

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

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

换句话说,您的选择是:

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

   您可以选择将后置条件添加到get访问器中Contract.Ensures(Contract.Result<string>() != null),但静态检查器不会以任何方式进行投诉.

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