算法导论 第二章 循环不变式(loop invariant)

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.
循环不变式(loop invariant)与数学归纳法(induction)进行对比:
When the first two properties hold, the loop invariant is true prior to every iteration of the loop. Note the similarity to mathematical induction, where to prove that a property holds, you prove a base case and an inductive step. Here, showing that the invariant holds before the first iteration is like the base case, and showing that the invariant holds from iteration to iteration is like the inductive step.
The third property is perhaps the most important one, since we are using the loop invariant to show correctness. It also differs from the usual use of mathematical induction, in which the inductive step is used infinitely; here, we stop the "induction" when the loop terminates.
利用循环不变式(loop invariant)来证明循环的正确性与用数学归纳法(induction)证明数学等式的相同点在于：需要验证初值，或初始状态是否满足条件。之后再证明在归纳或递推的过程中仍然满足这种条件。（这个条件在数学归纳中叫做递推关系，在循环中就是循环不变式(loop invariant)）。
循环不变式(loop invariant)与数学归纳法(induction)的区别在于：数学归纳可能是无限的，是无限地退的，但循环不变式所要证明的循环是要结束并给出正确结果的。

在插入排序的例子中：
INSERTION-SORT(A)
1 for j ← 2 to length[A]
2 do key ← A[j]
3 ▹ Insert A[j] into the sorted sequence A[1 ‥ j - 1].
4 i ← j - 1
5 while i > 0 and A[i] > key
6 do A[i + 1] ← A[i]
7 i ← i - 1
8 A[i + 1] ← key
· Initialization: We start by showing that the loop invariant holds before the first loop iteration, when j = 2.[1] The subarray A[1 ‥ j - 1], therefore, consists of just the single element A[1], which is in fact the original element in A[1]. Moreover, this subarray is sorted (trivially, of course), which shows that the loop invariant holds prior to the first iteration of the loop.
· Maintenance: Next, we tackle the second property: showing that each iteration maintains the loop invariant. Informally, the body of the outer for loop works by moving A[ j - 1], A[ j - 2], A[ j - 3], and so on by one position to the right until the proper position for A[ j] is found (lines 4-7), at which point the value of A[j] is inserted (line 8). A more formal treatment of the second property would require us to state and show a loop invariant for the "inner" while loop. At this point, however, we prefer not to get bogged down in such formalism, and so we rely on our informal analysis to show that the second property holds for the outer loop.
· Termination: Finally, we examine what happens when the loop terminates. For insertion sort, the outer for loop ends when j exceeds n, i.e., when j = n + 1. Substituting n + 1 for j in the wording of loop invariant, we have that the subarray A[1 ‥ n] consists of the elements originally in A[1 ‥ n], but in sorted order. But the subarray A[1 ‥ n] is the entire array! Hence, the entire array is sorted, which means that the algorithm is correct
在这个例子中，“At the start of each iteration of the for loop of lines 1-8, the subarray A[1 ‥ j - 1] consists of the elements originally in A[1 ‥ j - 1] but in sorted order.”，也就是，每当算法进行到第一行时，数组A中从第1个至第j-1个元素仍然是算法执行前数组中第1个至第j-1个元素，只是执行算法后，这些元素是排好序的，以上就是这个算法的for循环的循环不变式。(就是一个条件。)
再循环的Initialization阶段，j的初值为2，数组A[1 .. j-1]即是A[1],是排好序的，而且其元素仍然是原数组A[1]的，只是现在排好序了。
Maintenance：这个阶段要证明的是每一次循环的结果都满足先前提到的的循环不变式。
Termination：这个阶段要证明,当循环结束时，数组A中的所有元素都排好序。
再看算法第一行，当j=length[A]+1时循环结束，由于满足循环不变式，所以，数组A[1 .. length[A]]是排好序的，且是原数组的那些元素。
至此，可以说明算法正确。
再来说一下如何找循环不变式。由于算法是一步步执行的，那么如果每一步（包括初试和结束）都满足一个共同的条件，那么这个条件就是要找的循环不变式（loop invariant）。再说上面的例子，要得到的结果是排序且元素不改变的数组，所以循环不变式就是数组A中从第1个至第j-1个元素是排好序的且是与原数组的元素是一致的。