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

添加 「不變Ç==我==> b ==一個;」修復。由於dafny無法連接c，我和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"; 
}