I am reading loop invariant for insertion sort from the book Introduction to Algorithm by CLRS.
Pseudo code for the insertion sort is:
1 for i = 2 to n
2 key = A[i]
3 // Insert A[i] into the sorted subarray A[1:i-1]
4 j = i -1
5 while j>0 and A[j] > key
6 A[j+1] = A[j]
7 j = j-1
8 A[j + 1] = key
Here, Loop invariant is formally defined as below:
At the start of each iteration of the for loop of lines 1-8, the subarray
A[1:i-1]consists of the elements originally inA[1:i-1], but in sorted order.
To prove the correctness of algorithm, We have to show loop invariant is consistent at initialization, maintenance and termination.
Initialization: We start by showing that the loop invariant holds before the first
loop iteration, when i = 2. The subarray A[1:i-1] consists of just the
single element A[1], which is in fact the original element in A[1]. Moreover,
this subarray is sorted (after all, how could a subarray with just one value not
be sorted?), 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 for loop works by
moving the values in A[i-1],A[i-2],A[i-3] and so on by one position
to the right until it finds the proper position for A[i] (lines 4-7), at which point
it inserts the value of A[i](line 8).The subarray A[i:1] then consists of the
elements originally in A[1:i], but in sorted order. Incrementing i (increasing
its value by 1) for the next iteration of the for loop then preserves the loop
invariant.
A more formal treatment of the second property would require us to state and show a loop invariant for the while loop of lines 5-7. Let’s not get bogged down in such formalism just yet. Instead, we’ll rely on our informal analysis to show that the second property holds for the outer loop.
Termination: Finally, we examine loop termination. The loop variable i starts
at 2 and increases by 1 in each iteration. Once i ’s value exceeds n in line 1, the
loop terminates. That is, the loop terminates once i equals n + 1. Substituting
n + 1 for i in the wording of the loop invariant yields that the subarray A[1:n]
consists of the elements originally in A[1:n], but in sorted order. Hence, the
algorithm is correct.
My Question is about the Maintenance part. While overall idea for showing correctness of this algorithm is to prove for every i, the subarray A[1:i-1] is already sorted. If you have observed the Maintenance part, The sorting of element is being done till A[i]. Is this part still consistent with the formalized definition of loop-invariant?
A Loop Invariant is a property of a program loop that is true before (and after) each iteration.
In case of Insertion sort, the loop variant is -
Subarray A[1:i-1] is always sorted
Now, as you rightly said, during the iteration, the array will be sorted in range [1:i]. But the main mistake you are doing while analysing the algorithm is that the last statement of the outer loop iteration is increment of i. So, at the end of each iteration new value of i will be equal to i+1. Which will hold the truthfulness of loop invariant.
Update: just to clarify, initialization and termination depicts the start and end of the whole process, not each iteration. So, they will be checked only for i = 2 and i = n+1 respectively. Maintenance depicts each iteration. Now, at the end of each iteration, new value of i will be i+1. The statement "The subarray A[i:1] then consists of the elements originally in A[1:i], but in sorted order" comes before this increment. After the end of an iteration, I will be increased, which will again make statement "A[i:i-1] sorted" true.