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?

The invariant for the outer loop is sufficient, but first you need to prove that it's actually an invariant. For that, you need to provide and prove a precondition and postcondition for every statement inside the loop. And to prove a precondition and postcondition for the inner loop, you need another invariant.

To a human, it's fairly obvious that the inner loop correctly finds the place to insert the next element, and thus we can just use that in an informal argument. But, in formal semantics, we like boil proof to mechanical symbolic manipulations so that they can be checked by machine, and thus we can't do that. Whenever we encounter a statement, we must do as its rules dictate, and for loops, that means provide a loop invariant. See http://en.wikipedia.org/wiki/Hoare_logic for more details.

StackExchange Computer Science Q#6567, answer score: 5