循环不变式 Loop Invariant

循环不变式（量）

定义

循环不变量：S是一个语句，已知循环

while C do
E

当此循环满足以下条件，即：在任何循环开始前，语句S和C都为真，而且在循环结束后，S仍为真，那么S就是循环不变量。

定理

循环不变量定理：已知一个循环和循环条件的guard condition G。命 I(n) 为循环不变式。如果下面四个条件为真，那么此循环是正确的：

Basic property: the pre-condition implies I(0)
Induction property: for all ints k = 0, if guard and I(k) are true before the iteration, then I(k+1) is true after.
Eventual falsity of the guard: after a finite number of iterations, G becomes false.
Correctness of post-conditons: if N is the first place where G is false, and I(N) is true, then post-condition holds.

翻译：

基本属性：先验条件即 I(0)。
归纳属性：对于所有的整数 k = 0，如果守卫条件和 I(k) 都在迭代前成立，那么 I(k+1) 在迭代后也成立。
最终守卫条件不成立：经过有限的迭代次数后，守卫条件 G 不成立。
后验条件的正确性：如果 N 是第一个导致守卫条件 G 不成立的整数，且 I(N) 成立，那么后验条件也成立。

示例

guard condition G 是指在循环前对循环变量的检查，例如：while( i < n) 中的 i <= n。

以求数组中最大值为例子：

Max(A[1],...A[n])m = A[1]
i = 1
while(i <= n) do if A[i] > m then
m = A[i]
end if
i = i + 1
end whilereturn m

循环前的先验条件为数组的第一个元素 m = A[1] 而且 i = 1。循环的后验条件是m是数组A中最大的元素。那么现在的循环不变量就是I(i): m是数组A中前 i 个元素的最大值。The guard condition condition G is i <=n.

通过在i上的推导来证明这个循环的正确性。首先，注意n是个固定的整数，而且 i 的初始值比n小，且每次循环n都增加，在某一点的时候 i <=n 为假。这在n-1次循环之后总会发生。

现在来证明循环不变量。首先，I(1)是真的，因为A[1] = m，所以在数组中只有一个元素，所以此时A[1]肯定是最大的。

为了进行推导，我们假设m是A[1]…A[i]中的最大值，这个假设为I(i),我们要证明的是在一次循环之后，I(i+1)将会成立。

考虑两种情况：

A[i+1]>m，在这种情况下，A[i+1]比先前A中的元素都大，通过传递性，m=A[i+1]也是A[1]…A[i+1]中最大的元素。
A[i+1]<m，此时，m的值不变。

两种情况下，A[i+1] 都是 A[i]……A[i+1] 中的最大元素，故得证。

参考资料

[ORIGIN] 循环不变量(Loop invariant)

[VALUED] 从快速排序看循环不变量

[VALUED] 循环/递归算法正确性证明里如何选择「循环不变量」？

[VALUED] 循环不变性（loop invariant）-证明算法的正确性的一种方法

[VALUED] Loop Invariant Condition with Examples

[VALUED] Loop invariants | cs.cornell.edu