for j <- 2 to length(A) do // Invariant 1: A[1..j-1] is a sorted permutation of the original A[1..j-1] key <- A[j] i <- j-1 while (i > 0 and A[i] > key) do // Invariant 2: A[i .. j] are each >= key A[i+1] <- A[i] i <- i -1 A[i+1] <- key
First, we note that Invariant 1 is true initially because in the first iteration of the loop j = 2 so A[1..j-1] is A[1..1] and a single element is always a sorted list.
In order to show that Invariant 1 is maintained by the loop and true during the next iteration, we must examine the body of the loop. It must be true that after the last line of the outer loop (A[i+1] <- key), A[1..j] is a sorted permutation of the original A[1..j]. We will show this is true by examining Invariant 2 and reasoning from it.
Invariant 2 is true upon initialization (the first iteration of the inner loop) because i = j-1, A[i] was explicitly tested and know to be > key, and A[j] == key.
The inner loop maintains this invariant because the statement A[i+1] <- A[i] moves a value in A[i], known to be > key, into A[i+1] which also held a value >= key. Thus this statement does not change the validity of the invariant. (If after setting i <- i-1 the invariant does not hold, the loop test of A[i] > key catches the fact and terminates the loop.)
We also note that the inner loop does not destroy any data because the first iteration copies a value over A[j], the value stored in key. As long as key is stored back into the array, we maintain the statement that A[1..j] contains the first j elements of the original list.
Upon termination of the inner loop, we know the following things about the array A:
Given these facts, we see that A[i+1] <- key does not destroy any data and gives us A[1..j] is a sorted permutation of the original j elements of A.
Thus, Invariant 1 is maintained after an iteration of the loop and it remains to note that when the outer loop terminates, j = length(A) + 1 so A[1..j-1] is A[1..length], thus the entire array is sorted.