12

考虑这种不可变类型：

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

我在这里错过了什么吗？

4

2 回答 2

10

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

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

换句话说，您的选择是：

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

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

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

于 2010-07-30T00:47:13.570 回答
0

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

于 2015-08-13T19:09:51.707 回答