c# - 代码契约(Contract) - 没有正确警告只读成员？

Question

鉴于这门课，我不确定为什么我会收到 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 分析似乎对这个类非常满意；在构造函数中分配了一个非空值，并且 setter 需要非空值来更改_value因此确保被证明。

Answer 1

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

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

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