Дафни: Помогите правильному инварианту, уменьшите утверждение

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