Contract.Ensuresはどのように機能しますか？

Question

私はCode Contractsを使い始めていますが、Contract.Requiresはかなり簡単ですが、私はEnsuresが実際に何をしているのか分かりません。

私はこのような単純な方法で作成しようとしました：私は「間違った」のメッセージを見ることはない、またそれは例外または何かを投げるん

static void Main() 
{ 
    DoSomething(); 
} 

private static void DoSomething() 
{ 
    Contract.Ensures(false, "wrong"); 
    Console.WriteLine("Something"); 
} 

を。

これは実際に何をしていますか？

Answer 1

の場合は、適切な設定でリライタツールを実行しています。私の推測では、あなたは事後条件をチェックしないモードで走っているということです。

紛らわしいものを約Contract.Ensuresあなたがメソッドの開始時ににそれを書くということですが、それは、メソッドの最後にを実行します。リライタは、すべての魔法を実行して適切に実行され、必要に応じて戻り値が与えられます。

コード契約に関する多くの点と同様に、私はリライターツールの結果でリフレクターを実行することをお勧めします。あなたが正しい設定を持っていることを確認してから、リライタが何をしたのかを考えてください。

---

編集：私は、私はまだContact.Ensuresのポイントを表明していない実現。簡単に言えば、メソッドが最終的に何かを行ったことを確認することです。たとえば、リストに何かが追加されているか、戻り値がnullでないか、または何かであることが保証されます。たとえば、あなたが持つかもしれない：書き換えコードで

public int IncrementByRandomAmount(int input) 
{ 
    // We can't do anything if we're given int.MaxValue 
    Contract.Requires(input < int.MaxValue); 
    Contract.Ensures(Contract.Result<int>() > input); 

    // Do stuff here to compute output 
    return output; 
} 

を、返される値本当にが入力より大きいことを保証するために、リターンの時点でチェックがあるでしょう。