3

鉴于此类，我不确定为什么会收到 Ensure unproven Result != null 警告。

public class MyClass {
  private readonly string _value;

  public MyClass(string value) {
    Contract.Requires(value != null);  
    _value = value;
  }

  public string Value {
    get {
      Contract.Ensures(Contract.Result<string>() != null);
      return _value;
    }
  }
}

我可以通过添加 _value != null 的不变量来消除警告，但感觉我不应该这样做。这只是分析的限制吗？

编辑：为问题添加更多内容，因为我认为我的问题的重点被遗漏了。

public class Test {
    private string _value = "";

    public string Value {
        get {
            Contract.Ensures(Contract.Result<string>() != null);
            return _value;
        }
        set {
            Contract.Requires<ArgumentNullException>(value != null);
            _value = value;
        }
    }
}

CC 分析似乎对这个类非常满意；在ctor中分配了一个非空值，因此证明Requires了要更改的setter非空值。_valueEnsures

4

2 回答 2

1

您的构造函数不承诺 _value将是非空的。它设置_value为value，它是非空的，但这是一个实现细节，而不是合同的一部分。即使它是合同的一部分，也不够，因为当您添加另一个不做出相同承诺的构造函数时，所有前置条件和后置条件都应该保持同样有效。

您应该添加不变量 that _value != null。为什么感觉你不应该这样做？

编辑：作为替代方案，您可以尝试添加一个不变量Value != null（这在 之外也很有用MyClass），并使Value' 的属性获取器确保Contract.Result<string>() == _value（仅证明不变量），但我不确定这会起作用。

于 2012-06-09T15:40:47.597 回答
1

在提出问题时不确定该选项是否可用，但我今天遇到了类似的问题，发现通过打开代码合同选项“Infer Invariants for readonly”，警告消失了。

于 2014-03-07T05:46:44.433 回答