确定循环不变量？

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 是循环不变量。在每次循环重复之前和之后始终为真。

循环不变量在进入循环时应该为真，并得到保证 在循环的每次迭代后保持真实。这意味着在 从循环中退出循环不变量和循环终止 条件可以保证。

查看 Floyd-Hoare 逻辑部分，其中包含简单的 xhttp://en.wikipedia.org/wiki/Loop_invariant

Answer 3

您对循环不变量的定义并不完全正确。本质上，它应该只在每次循环重复之前和之后才成立。维基百科have nice definition.

这个循环的不变量是：the values[x] and values[x + 1] are maybe not sorted or x is the last index 在每次循环迭代之前和之后都是真的。而且它仍然是真的就在循环之后结合false for 循环条件：

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

自然，循环不变量应该与循环体及其执行的任务相关。循环不变量确保在循环的每个步骤中，循环体执行的条件相同。