一般而言,用这个式子表示希望得到的结果,如果在循环的每一步,这个式子都是正确的,那么循环结束后,这个式子也正确,并得到了期望的结果.

lenovo所引用的文章里的例子是这样的:

QUOTE:

apvector<int> list(n); // n is some positive integer

int k, indexMax;

<code which assigns values to all entries in list>

indexMax = 0;

for(k = 1; k < list.length(); k++){

// invariant true here

if (list[k] > list[indexMax])

indexMax = k;

}

这是一个很简单的求最大值(在数组中的下标)的问题,在循环内// invariant true here 处可以指明始终成立的不变式为:

QUOTE:

在当前的k之前, 最大值的下标是indexMax, 而且0<=indexMax<k

可以看出这个式子在整个循环过程中是始终成立的,所以在循环结束的时候(k=list.length()),这个式子也成立,

即:

QUOTE:

在整个list中,最大值的下标是indexMax, 而且0<=indexMax<list.length()

这就是我们期望得到的结果,也就是说我们得到了最大值的下标

循环不变式有3个性质：

初始化：在第一次循环前是正确的

保持：在循环迭代中是正确的

终止：当循环结束时也是正确的

根据循环不变式的3个特性，再结合归纳法，证明我们写的循环是正确滴。

一句话：,如果在循环的每一步,这个式子都是正确的,那么循环结束后,这个式子也正确

算法导论中的循环不变性(loop invariant)

算法导论第二章中的原文是：We state these properties of A[1 ‥ j -1] formally as a loop invariant。其中举的例子是插入排序，每次循环从数组A中取出第j个元素插入有序区A[1 .. j-1]，然后递增j。这样A[1 .. j-1]的有序性始终得到保持，这就是所谓的“循环不变”了。
这个概念主要用来检验算法的正确性。原文如下：
We use loop invariants to help us understand why an algorithm is correct. We must show three things about a loop invariant:
Initialization: It is true prior to the first iteration of the loop.
Maintenance: If it is true before an iteration of the loop, it remains true before the next iteration.
Termination: When the loop terminates, the invariant gives us a useful property that helps show that the algorithm is correct.
1. 初始化（循环第一次迭代之前）的时候，A[1 ‥ j -1]的“有序性”是成立的；
2. 在循环的每次迭代过程中，A[1 ‥ j -1]的“有序性”仍然保持；
3. 循环结束的时候，A[1 ‥ j -1]的“有序性”仍然成立。
另外，我个人认为应该翻译为“循环不变性”，“循环不变式”是一种误导。因为这是一种性质，一种属性（property），而不是表达式。