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;
    }
}

ここで注意すべき2つのこと：

  • 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.Pathnullにすることはできません（設定には対応するコントラクトが不変であるため）
  • したがって、に割り当てることによりsettings.Path、_pathnullに_pathすることはできません

私はここで何かを逃しましたか？

4

2 に答える 2

10

コード コントラクト フォーラムを確認したところ、開発者の 1 人から次のような回答が寄せられた同様の質問が見つかりました。

あなたが経験している動作は、進行中のメソッド間推論によって引き起こされていると思います。静的チェッカーは、最初にコンストラクターを分析し、次にプロパティ、メソッドを分析します。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 に答える