確定循環不變？

Question

我不太明白如何確定循環不變量。我知道它在循環之前，循環之後，以及在每次循環迭代期間都是真實的，但是它就是這樣。這是我正在處理的一個示例問題，你如何找到這個循環不變的問題？

i, temp : integer; 
values : array[1..100] of integer; 

x := 1; 

while x < 100 loop 

if values[x] > values[x+1] then begin 

temp := values[x]; 

values[x] := values[x+1]; 

values[x+1] := temp; 

end if; 

x := x + 1; 

end loop; 

Answer 1

簡而言之，循環不變是一些謂詞（條件），對於循環的每次迭代都保持良好（真）。

在你的情況下，循環不變將是：

x >= 1 && x < 100

考慮終止條件，上述表達式將始終保持true整個循環。如果它變成false，則循環結束。

Answer 2

1 <= x <= 100是循環不變量。在每個循環重複之前和之後總是如此。

在進入循環時應保持循環不變，並保證 在循環的每次迭代後保持爲真。這意味着在 退出循環時，循環不變量和循環終止條件都可以得到保證。

見與簡單的X < 10環例如弗洛伊德 - 霍爾邏輯部分：http://en.wikipedia.org/wiki/Loop_invariant

Answer 3

循環不變的你定義並不完全正確。從本質上講，只有在每次循環重複之前和之後才應該如此。 WikiPedia have nice definition。

此循環的不變量爲：the values[x] and values[x + 1] are maybe not sorted or x is the last index在每次循環迭代之前和之後都是如此。而且它還是真正後右環與false相結合的循環狀態：

i, temp : integer; 
values : array[1..100] of integer; 

x := 1; 

while x < 100 loop 
    // the values[x] and values[x + 1] are maybe not sorted or x is the last index - true 
    if values[x] > values[x+1] then begin 
     temp := values[x]; 
     values[x] := values[x+1]; 
     values[x+1] := temp; 
    end if; 
    x := x + 1; 
    // the values[x] and values[x + 1] are maybe not sorted or x is the last index - true 
end loop; 

// the values[x] and values[x + 1] are maybe not sorted or x is the last index - true 
// and x >= 100 - true 

自然，循環不變應與循環體和要執行的任務。循環不變保證循環的每一步都有相同的條件供循環體執行。