線性陣列搜索的循環不變式

Question

int i = 0 
boolean answer = false 
while (i < a.length) { 
    if a[i] == 0 
     answer = true 
    i = i + 1 

其中'a'是一個整數數組。 我正在做一個問題文件，它問我這是什麼循環不變，我已經確定代碼算出數組是否包含0。但到目前爲止，我只能想到不變爲

i <= a.length 

和問題陳述包括變量我，a和答案在不變量中，所以我知道這是不對的。我還沒有遇到過涉及布爾變量的循環不變式，並且感到困惑，誰能幫助解釋？

Answer 1

這是你在微軟Dafny循環與適當的循環不變的實施規定：

method Main(a:array<int>) returns (answer:bool) 
    requires a != null 
    ensures answer <==> (exists i :: 0 <= i < a.Length && a[i] == 0) 
{ 
    var i:int := 0; 
    answer := false; 
    while (i < a.Length) 
    invariant 0 <= i <= a.Length; 
    invariant !answer ==> !(exists j :: 0 <= j < i && a[j] == 0) 
    invariant answer ==> (exists j :: 0 <= j < i && a[j] == 0) 
    { 
    if a[i] == 0 { 
     answer := true; 
    } 
    i := i + 1; 
    } 
} 

您可以在online version of Dafny