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";
}