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

while C   do

 E

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

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

        1）Basic property: the pre-condition implise  I(0)

2）Induction property: for all ints k = 0, if guard and I(k) are true before the iteration, then I(k+1) is true after.

3）Eventual falsity of the guard: after a finite number of iterations, G becomes false;

4）Correctness of postconditons: if N is the first place where G is false, and I(N) is true, then post-condition holds.

其中，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 while

return 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)将会成立。考虑两种情况，1)A[i+1]>m，在这种情况下，A[i+1]比先前A中的元素都大，通过传递性，m=A[i+1]也是A[1]......A[i+1]中最大的元素。

2)A[i+1]<m，此时，m的值不变。