# Loop invariants?

Insertion-Sort (A) [where A is an array of numbers to be sorted]

(1) for j = 2 to A.length
(2)       key = A[j]
(3)       i = j -1
(4)       while i > 0 and A[i] > key
(5)              A[i+1] = A[i]
(6)              i = i - 1
(7)       A[i + 1] = key


CLRS proves the correction of the above algorithm by using a loop invariant:

Loop Invariant: 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.

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

Termination: When the loop terminates, the invariant gives us a useful property that helps show that the algorithm is correct.

In the explanation of the maintenance aspect of the loop invariant, the following is mentioned:

Maintenance: A more formal treatment of the this property would require us to state and show a loop invariant for the while loop of lines 5–7. 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.

Why would a "formal treatment" require a loop invariant for the while loop? Having one invariant for the outer for loop is sufficient to prove the correctness of the algorithm- why would a "formal treatment" require a loop invariant?

-
I don't see any loop invariant here. Can you tell us how are you using it here? –  Shashwat Nov 9 '12 at 4:46