代码协定 - 未正确警告只读成员

Question

鉴于这个类，我不确定为什么我得到确保未经证实的结果！=空警告。

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 中分配了一个非空值，并且 setter Requires非空值来更改_value从而证明Ensures。

Answer 1

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

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

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

Answer 2

不确定在

提出问题时该选项是否可用，但我今天遇到了类似的问题，发现通过打开代码协定选项"推断只读的不变量"，警告消失了。