Loop invariants

A loop changes its values many times, so it is hard to reason about all at once. The method is to find one statement about those values that is true every time the loop reaches its first line. Then you only have to reason about one pass.

A statement that stays true

A loop invariant is a statement about the loop’s values that is true at the start of every pass. The values change, but the statement stays true.

Here is the loop for the largest value, with its invariant written as a comment:

def largest(a):
    best = a[0]
    i = 1
    # Invariant: best is the largest of a[0..i-1]
    while i < len(a):
        if a[i] > best:
            best = a[i]
        i += 1
    return best

a[0..i-1] means the values from index 0 to index i - 1, both included. These are the values the loop has already looked at.

Three things to prove

To use an invariant, you prove three things:

1. Start. The statement is true before the first pass.
2. Keep. If it is true at the start of a pass, it is still true at the start of the next pass.
3. Finish. When the loop ends, the statement, together with the reason the loop ended, gives the promise in the spec.

Parts 1 and 2 together show that the statement is true at the start of every pass, however many passes there are. This is the same idea as proof by induction, which lesson 3 covers.

Example: the largest value

1. Start. Before the first pass, i = 1 and best = a[0]. The only value seen is a[0], and it is the largest of itself. True.
2. Keep. Suppose best is the largest of a[0..i-1]. The pass compares a[i] with best and keeps the bigger one. So afterwards best is the largest of a[0..i]. Then i goes up by 1, and the statement reads the same as before. True.
3. Finish. The loop ends when i = len(a). Then the invariant says best is the largest of a[0..len(a)-1], which is the whole list. That is the promise.

Step through the figure. The blue bracket covers the values already seen, and the check under the list tests the invariant after every step. Then switch to the version that starts with best = 0 on a list of negative numbers. Part 1 fails at once, and nothing later repairs it.

Choosing a good invariant

A useful invariant usually describes the part of the job already done. Ask: “if I stopped the loop right now, what would I know?” Some patterns come up often:

Sometimes the obvious statement is too weak to prove part 2. Then you must make it say more. For example, to track the best sum of a stretch of consecutive values, “best is the best sum so far” is not enough. You also need a second statement: “cur is the best sum of a stretch that ends at the current value”. Practice problem 5 uses exactly this.

Proving the loop stops

An invariant shows that the answer is right if the loop ends. To show it does end, find a whole number that gets smaller on every pass and can never go below zero. Such a number is sometimes called a variant.

In the loop above, the number is len(a) − i. Every pass adds 1 to i, so it gets smaller by 1. It starts at n − 1 and cannot go below 0. So there are at most n − 1 passes. In binary search the number is the size of the window.