loops - 确定循环不变量？

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

1 <= x <= 100 is the loop invariant. Always true before and after each loop repitition.

A loop invariant should be true on entry into a loop and is guaranteed to remain true after every iteration of the loop. This means that on exit from the loop both the loop invariant and the loop termination condition can be guaranteed.

See the Floyd-Hoare logic section with simple x<10 loop example: http://en.wikipedia.org/wiki/Loop_invariant

Answer 2

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

这个循环的不变量是：the values[x] and values[x + 1] are maybe not sorted or x is the last index在每次循环迭代之前和之后都是真的。在循环结合for 循环条件之后它仍然是正确的：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

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

Answer 3

简单来说，循环不变量是一些谓词（条件），对于循环的每次迭代都保持良好（真）。

在您的情况下，循环不变量将是：

x >= 1 && x < 100

给定终止条件，上述表达式将始终保留true在整个循环中。如果变为false，则循环结束。