functional-programming - Dafny: 適切な不変式を支援し、ステートメントを減らします

Question

ここで何が問題なのか誰でも助けてくれますか。このプログラムを検証すると、以下のエラーが発生します。

いろいろ試してみましたが、検証に合格しません。助けてください。

method Main() {
     var a:int := 0;
     var b:int := -1;
     var c:int := 0;
     var i:int := 100;
     while (a!=b)
     invariant 0<=c<i
     decreases i-c
     {
         b := a;
       c := c+1;
         if (c < i) {
           a := a+1;
         }
     }
    print "Eureka";
}

…………

stdin.dfy(7,19): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
    (0,0): anon0
    stdin.dfy(6,6): anon12_LoopHead
    (0,0): anon12_LoopBody
    stdin.dfy(6,6): anon13_Else
    stdin.dfy(6,6): anon15_Else
    (0,0): anon16_Else
    (0,0): anon10

Dafny program verifier finished with 1 verified, 1 error

Answer 1

「不変 c == i ==> b == a;」を追加 それを修正しました。dafny が c,i と b,a の間をリンクできなかったためです。

method Main() {
     var a:int := 0;
     var b:int := -1;
     var c:int := 0;
     var i:int := 100;
     while (a!=b)
     invariant 0<=c<=i
     invariant c == i ==> b == a;
     decreases i-c
     {
         b := a;
         c := c+1;
         if (c < i) {
           a := a+1;
         }
     }
    print "Eureka";
}