Loop Invariant/循环不变量

Loop Invariant - a property of a program loop that is true before (and after) each iteration

From: Wikipedia - Loop invariant

EN

Introduction to Algorithm

In the book Introduction to Algorithm, loop invariant is included in chapter 2.1, which is in the insertion sort. Loop invariant is employed to establish the correctness of the algorithm, which is also able to be applied on other algorithms.

Three conditions must to be held true:

  1. Initialization: It is true prior to the first iteration of the loop
  2. Maintenance: If it is true before an iteration of the loop, it remains true before the next iteration.
  3. Termination: When the loop terminates, the invariant gives us a useful property that helps show that the algorithm is correct.

In the case of insertion sorting, the loop invariant is:

At the start of each iteration of the for loop of line 1-8, the subarray consists of the elements originally in , but in sorted orders.

three conditions became:

  1. Initialization: We start by showing that the loop invariant holds before the first loop iteration, when . The subarray , therefore, consists of just the single element , which is in fact the original element in . Moreover, this subarray is sorted (trivially, of course), which shows that the loop invariant holds prior to the first iteration of the loop.

    In plain word, this is saying, before the iteration starts, there is only one element in the sorted subarray, and therefore it’s sorted which satisfies the condition.

  2. Maintenance: Next, we tackle the second property: showing that each iteration maintains the loop invariant. Informally, the body of the for loop works by moving , and so on by one position to the right until finds the proper position for , at which point it inserts the value of . The subarray then consists of the elements originally in , but in sorted order. Incrementing for the next iteration of the for loop then preserves the loop invariant.

    This is saying that, with each iteration, the values before current value are sorted.

  3. Termination: Finally, we examine what happens when the loop terminates. The condition causing the for loop to terminate is that . Because each loop iteration increases by 1, we must have at that time. Substituting for in the wording of loop invariant, we have that the subarray consists of the elements originally in , but in sorted order. Observing that the subarray is the entire array, we conclude that the entire array is sorted. Hence, the algorithm is correct.

    When the loop ends, each element is iterated; the whole array is sorted. Consequently, the termination determines the correctness of the algorithm.


Other Explanation

I found that the example from wikipedia and What is a loop invariant? is very easy to understand.

Wikipedia

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
int max(int n,const int a[]) {
int m = a[0];
// m equals the maximum value in a[0...0]
int i = 1;
while (i != n) {
// m equals the maximum value in a[0...i-1]
if (m < a[i])
m = a[i];
// m equals the maximum value in a[0...i]
++i;
// m equals the maximum value in a[0...i-1]
}
// m equals the maximum value in a[0...i-1], and i==n
return m;
}

StackOverflow

1
2
3
int j = 9;
for(int i=0; i<10; i++)
j--;

In this example it is true (for every iteration) that i + j == 9. A weaker invariant that is also true is that && .


CN

Introduction to Algorithm


Reference

Introduction to Algorithm

Loop invariant

What is a loop invariant?

-------The end of this article  Thank you for your reading-------
0%