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 という Invariant を追加することで警告を消すことができますが、そうする必要はないように感じます。これは分析の単なる制限ですか？

編集：私の質問のポイントが見逃されていると思うので、質問にもう少し追加します。

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 には null 以外の値が割り当てられており、setterRequiresの null 以外の値が変更_valueされることEnsuresが証明されています。

4

2 に答える 2

1

_valueコンストラクターは、それがnull以外になることを約束しません 。nullではないに設定_valueされますがvalue、これは実装の詳細であり、コントラクトの一部ではありません。それが契約の一部であったとしても、それだけでは十分ではありません。同じ約束をしない別のコンストラクターを追加すると、すべての事前条件と事後条件が等しく有効なままになるはずだからです。

その不変条件を追加する必要があり_value != nullます。なぜあなたはそうする必要がないように感じるのですか？

編集：別の方法として、Value != null（の外でも役立つMyClass）不変条件を追加して、ValueのプロパティゲッターにContract.Result<string>() == _value（単に不変条件を証明するために）確実にすることができますが、それが機能するかどうかはわかりません。

于 2012-06-09T15:40:47.597 に答える
1

質問がされたときにオプションが利用可能だったかどうかはわかりませんが、今日同様の問題に遭遇し、コード コントラクト オプション「読み取り専用の不変条件を推測する」をオンにすると、警告が消えたことがわかりました。

于 2014-03-07T05:46:44.433 に答える