dafnyの2つのintに不変式を掛ける簡単な方法

Question

このQ3メソッドは、res | n0 |にm0を追加することによってn0 * m0を通勤させます。回。 n0が負の場合、n0とm0の両方をn0 * m0 = -n0 * -m0のように反転させます。

問題は、不変量がブール型である必要があるため、私のインバリアントがどのように見えるかを正確にはわからないということです。誰かが不変のブール条件がどのように見えるか教えていただけますか？私はAbs((n0)-n)*m == resについて考えましたが、うまくいきません。

method Q3(n0 : int, m0 : int) returns (res : int) 
    ensures n0*m0 == res 
{ 

    var n, m : int; 
    res := 0; 
    if (n0 >= 0) 
    {n,m := n0, m0;} 
    else 
    {n,m := -n0, -m0;} 

    while (0 < n) 
    invariant Abs((n0)-n)*m 
    { 
    res := res + m; 
    n := n - 1; 
    } 
} 

function Abs(x: int): int 
{ 
    if x < 0 then -x else x 
} 

Answer 1

ループ不変量を設計しようとするときには、まず逆方向に作業すると便利です。ループ終了後に何を知る必要がありますか？

この方法では、ループが終了すると、ポストコンディションn0 * m0 == resを確立する必要があります。これがループ不変量の開始点です。

resはループによって変更されるため、n0 * m0 == res自体は不変ではありません。代わりに、ループがこの目標に向かってどのように「進歩するか」を考える必要があります。このループは、mをresに追加することによって進行します。そのため、おおよその合計でn回です。 nが0の場合、ループは終了します。

ここでは一般的なパターンが便利です。不変式は、「これまでに」何が行われたのか、「何が残されているのか」について話す必要があります。この場合、これまでに行われていることはresであり、残るのは残りのnの追加でmです。ループの各反復は、残された1つの作業を取り、それを実行して不変量を維持する。

つまり、このループの良好な不変量はres + n * m == n0 * m0です。

また、Dafny Tutorialにはループインバリアントに関するセクションがあり、役立つ可能性があります。