Proving a loop right: the invariant

A sentence that is true before the loop, stays true through every pass, and says something useful when the loop stops.

Testing a loop tells you it worked on the inputs you supplied. To know it works on every input, you need an argument, and the argument has a fixed shape: find one sentence about the loop's variables that is true every time the loop is at the top, and check that the sentence, plus the reason the loop stopped, forces the answer to be right.

Start with the maximum scan from the first lesson, printed at the top of every pass so you can watch the sentence hold.

The two columns are never different. The sentence they agree on is: `best` holds the largest of the readings at positions 0 up to `i - 1`. That sentence is the point of the loop, and it is true at the top of every pass, whatever the data.

The three obligations

A loop invariant is a statement about the program's variables that is true every time control reaches the top of the loop. To use one as a proof you discharge three obligations, and each one is a separate small argument.

1. Initialisation. The statement is true the first time the loop is reached, before any pass has run.
2. Maintenance. If the statement is true at the top of a pass and the loop's condition is true, then it is true again at the top of the next pass, after the body has run.
3. Termination. The loop does stop, and when it does, the statement together with the reason it stopped gives you what the algorithm promised.

Here is the whole argument for the maximum scan, with nothing left out. The invariant is: at the top of the loop, best is the largest value among positions 0 to i - 1.

• Initialisation. Before the first pass, i is 1 and best is readings[0]. The positions 0 to 0 hold one value, and the largest of one value is that value, so the invariant holds.
• Maintenance. Suppose at the top of a pass best is the largest among positions 0 to i - 1, and i < n so the body runs. The body compares readings[i] with best and keeps whichever is larger, so afterwards the variable holds the largest among positions 0 to i. Then i becomes i + 1, so the claim about positions 0 to (new i) minus 1 is exactly what has been established. The invariant holds at the top of the next pass.
• Termination. Each pass increases i by 1 and the condition is i < n, so after at most n - 1 passes the condition fails and the loop stops. It stops with i equal to n, and the invariant then says best is the largest among positions 0 to n - 1, which is every position. That is the postcondition.

Insertion sort

The same three obligations carry a much less obvious loop. Insertion sort builds a sorted arrangement the way most people sort a hand of cards: take the next card, slide it left past every card bigger than it, and drop it into the gap. Run it and watch what the front of the array looks like after each outer pass.

Two things are true of every printed line. The first i + 1 entries are in increasing order, and those entries are the same values the array started with in those positions, rearranged. Neither is true of the entries further right, which have not been touched.

That gives the invariant for the outer loop: at the top of the outer loop, positions 0 to `i - 1` hold the values that originally sat in positions 0 to `i - 1`, arranged in increasing order. Notice it has two halves. Sorted is not enough on its own, because a loop that overwrote the front with zeros would leave it sorted and would have lost the data.

• Initialisation. At the first arrival i is 1, so the claim is about positions 0 to 0: one value, still the value it started as, and a single value is in increasing order. True.
• Maintenance. Assume positions 0 to i - 1 hold the original values of those positions in increasing order. The body saves key = a[i], then shifts every entry greater than key one place to the right, walking left from i - 1. Shifting moves values without losing them, and it only moves entries strictly greater than key. The loop stops when it meets an entry not greater than key, or when it runs off the left end. Either way the gap it leaves is at a position where everything to the left is at most key and everything to the right is greater than key. Writing key into the gap therefore leaves positions 0 to i in increasing order, holding exactly the original values of positions 0 to i. Then i increases by 1, which restores the invariant word for word.
• Termination. The outer loop increases i each pass and stops when i reaches n, so it stops after n - 1 passes. At that moment the invariant says positions 0 to n - 1, which is the whole array, hold the original values in increasing order. That is the definition of having sorted it.

Invariants earn their keep when a loop is subtly wrong, because a broken invariant points at the exact line. Here the inner condition is j > 0 rather than j >= 0, one character different. Predict what the printed lines will look like before you run it.

The invariant fails at the first pass where the new value belongs at position 0, because the inner loop refuses to walk past position 1 and the value is dropped one place too far right. Maintenance is the obligation that breaks, and it breaks on exactly the case the condition excluded.