単純な方法の事後条件が成立しない可能性があります

Question

私はこの単純な方法でDafnyに問題があり、なぜ動作しないのか分かりません。デバッガはないので、私はこの言語には新しく、誰かが助けてくれることを願っています。

事後条件は、このリターンパスに保持しない場合があります：私は、次の取得マイクロソフトdafnyコンパイラでそれを実行すると、私は..

method Q2(x : int, y : int) returns (big : int, small : int) 
    ensures big > small; 
{ 
    if (x > y) 
    {big, small := x, y;} 
    else 
    {big, small := y, x;} 
} 

仕様が不完全だと思います。 （行8） これは保持できない事後条件です。 （行2）

Answer 1

問題は、xとyが等しい可能性があります。この場合、bigとsmallも同じになります。

ポストコンディションをbig >= smallに変更することで修正できます。または、発信者がxとyを今まで通り渡ることを禁止したい場合は、x != yを必要とする前提条件を追加できます。