Let us see how these properties hold for insertion sort.
-
Initialization:We start by showing that the loop invariant holds before the first loop iteration, when j = 2.[1] The sub array 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 sub array 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 sub array 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.
