Contract.Ensuresのカスタムメソッド

Question

私はコード契約をもう少し詳しく理解しようとしています。私はtry/getパターンの不変条件をアサートしようとしていますが、trueを返し、outオブジェクトがnullでない場合は、falseを返します。

public static bool TryParseFruit(string maybeFruit, out Fruit fruit) 
    { 
     Contract.Requires(maybeFruit != null); 

     Contract.Ensures((Contract.Result<bool>() && Contract.ValueAtReturn(out fruit) != null) || 
         (!Contract.Result<bool>() && Contract.ValueAtReturn(out fruit) == null)); 

     // Elided for brevity 
     if (ICanParseIt()) 
     { 
      fruit = SomeNonNullValue; 
      return true; 
     } 
     else 
     { 
      fruit = null; 
      return false; 
     } 
    } 

私はので、私はこのために私自身の方法を考慮したかったContract.Ensures内の重複を好きではありません。

[Pure] 
public static bool Implies(bool a, bool b) 
{ 
    return (a && b) || (!a && !b); 
} 

は、その後、私は

Contract.Ensures(Implies(Contract.Result<bool>(), Contract.ValueAtReturn(out fruit) != null); 

にTryParseFruitで私の不変を変えしかし、これは「証明されていない保証します」という警告を生成します。私がImpliesメソッドでインラインリファクタリングを実行すると、すべてが再びOKです。

誰かが私になぜこれが起こるのか説明できますか？ Contract.ValueAtReturnが何らかの方法で魔法のように使用されているため、結果を別の関数に渡して動作させることができないことを意味するので、私はそれを推測しています。

（更新＃1）

私は、次のContract.Ensuresのすべてが同じことを表現することを考えて（つまり関数は、その後trueを返す場合fruitがそうでなければ、非NULLであることをfruitはnullです）。私は一度にこれらのいずれかを使用していたことに注意してください:)

Contract.Ensures(Implies(Contract.Result<bool>(), Contract.ValueAtReturn(out fruit) != null));   
Contract.Ensures(Contract.Result<bool>() == (Contract.ValueAtReturn(out fruit) != null)); 
Contract.Ensures(Contract.Result<bool>()^(Contract.ValueAtReturn(out fruit) == null)); 

ただし、以下のコードのクリーン・コンパイルに上記Contract.Ensures鉛を全く。私はCode.Contractsがfruit.Nameはnull参照することはできないことを表現したい。

Fruit fruit; 
    while (!TryGetExample.TryParseFruit(ReadLine(), out fruit)) 
    { 
     Console.WriteLine("Try again..."); 
    } 

    Console.WriteLine(fruit.Name); 

私は、上記の詳細な表現方法を使用すれば、完全にクリーンなコンパイルをコード契約で取得できます。私の質問はなぜです！

Answer 1

もちろん、試してみることもできますContract.Ensures(Contract.Result<bool>() == (Contract.ValueAtReturn(out fruit) != null));アナライザが他の演算子よりも好きなことをあいまいに思い出しています。

私はこれらのことをContract.Assertとトレースすることで、分析の穴がどこにあるのかを知るのに役立ちました。私はまた、Contract.Assertが分析を成功させるケースを発見しました。言い換えれば、あなたはいくつかのアサーションでこれを解決するかもしれません：

public static bool TryParseFruit(string maybeFruit, out Fruit fruit) 
{ 
    Contract.Requires(maybeFruit != null); 

    Contract.Ensures(Implies(Contract.Result<bool>(), Contract.ValueAtReturn(out fruit) != null); 

    // Elided for brevity 
    if (ICanParseIt()) 
    { 
     fruit = SomeNonNullValue; 
     Contract.Assert(Implies(Contract.Result<bool>(), Contract.ValueAtReturn(out fruit) != null); 
     return true; 
    } 
    else 
    { 
     fruit = null; 
     Contract.Assert(Implies(Contract.Result<bool>(), Contract.ValueAtReturn(out fruit) != null); 
     return false; 
    } 
} 

私は知っています。一方、アサーションが失敗した場合は、たとえば、ロジックの他の面を見ることができます。たとえば、Contract.Assert(SomeNonNullValue != null);でコードを捨てて、分析器が非ヌルネスについて確実性を失う場所を確認することができます。SomeNonNullValue

EDIT

Assertが証明されていないが、あなたはそれが証明可能であることを知っているならば、あなたは問題を特定するためにそれを使用することができます。私は、問題（またはそれの少なくとも一部）が、のあなたの欠如であると考えています。Impliesメソッドです。 Contract.Ensures(Contract.Result<bool>() == (Contract.OldValue(a) == Contract.OldValue(b)));を追加してみてください。また、論理演算子ごとに異なる処理について曖昧な思い込みがある場合は、そのメソッドの復帰を再試行してみてください。例：return a == b;

Answer 2

まず第一に、あなたの状態は、カスタムメソッドを使用せずに圧縮することがあります：

Contract.Ensures(Contract.Result<bool>()^(Contract.ValueAtReturn(out fruit) == null)); 

（ここで^がXOR operatorある）

今、あなたの質問について。静的ベリファイアがどのように機能しているかを正確に知っていない限り、その理由が何であるかを言うことは非常に難しいと思います。何百もの制限があるかもしれません。私の視点から見ると、Code Contracts検証者は、メソッドの境界で何とか止まる。私は、検証者がImpliesメソッドを調べておらず、何をしているのかわからないということです。したがって、それぞれの場合に何が返されるかを導き出すことはできません。メソッドをインライン化すると、コードを完全にチェックすることができます。しかし、やはり、デベロッパーチームの外の誰も正確に分かっていないと思います。

UPDATE

それはコメントで考え出してきたように、XOR演算子は、現在のCodeContractsのリリースでサポートされていないことのようです。次回より良い運を...