Correctness: specifications and loop invariants

The last lesson asked for one sentence explaining why each faster solution is right. This lesson makes that sentence precise. It shows how to say exactly what a function promises, and how to argue that a loop keeps the promise for every input, not only for the inputs you happened to test.

Say what the function promises

A specification has two parts:

• the precondition: what must be true of the input when the function is called;
• the postcondition: what will be true of the result when it returns, provided the precondition held.

For a function largest(items), a careful specification reads:

• Precondition: items is a list of numbers with at least one item.
• Postcondition: the result is one of the items, and no item is larger than it.

Both halves of the postcondition matter. “No item is larger” alone would let the function return a huge number that is not in the list at all. And the precondition is not decoration: Python’s own max() has the same one, and called on an empty list without a default it raises ValueError rather than inventing an answer. A caller who breaks the precondition gets no promise.

Loop invariants

Most algorithms are loops, and a loop is where a promise is easiest to break. A loop invariant is a statement about the loop’s variables that is true every time the loop test is checked: before the first pass, and again after each pass. For the loop inside largest, a good invariant is:

Invariant: best is the largest of items[0:i].

To show that a loop is correct with an invariant, check three things:

1. Initialisation. It is true before the first pass. With best = items[0] and i = 1, it says that best is the largest of the first item alone, which is true.
2. Maintenance. If it is true before a pass, it is true after it. The body compares items[i] with best and keeps the larger, then adds 1 to i, so best is again the largest of the first i items.
3. Termination. The loop stops, and when it does, the invariant together with the reason it stopped gives the postcondition. It stops when i == len(items), and then “the largest of items[0:i]” is the largest of all of them.

This is an argument about every possible input at once. Tests can only ever try some of them.

C. A. R. Hoare made the method formal in “An axiomatic basis for computer programming” (Communications of the ACM, volume 12, number 10, pages 576–580), building on Robert Floyd’s earlier work with flowcharts. He wrote a precondition, a program and a postcondition together, and gave a rule for while loops built on an invariant P. In the notation used today:

In words: if every run of the body S that starts with P true and the loop condition B true ends with P true again, then the whole loop, started with P true, can only end with P still true and B false. The three checks above are this rule applied by hand, plus the reason the loop ends at all, which the rule leaves out (more on that below).

Assertions put the invariant to work

An assert statement checks a condition while the program runs and raises AssertionError when it is false. Writing the invariant as an assertion turns the argument into something the computer checks on every pass:

def largest(items):
    """Precondition: items is a list of numbers with at least one item.
    Postcondition: the result is one of the items, and no item is larger."""
    best = items[0]
    i = 1
    while i < len(items):
        # Invariant: best is the largest of items[0:i].
        assert best == max(items[:i]), f"invariant broken at i={i}"
        print(f"i={i}: best={best} is the largest of {items[:i]}")
        if items[i] > best:
            best = items[i]
        i += 1
    # The invariant still holds, and the loop stopped because i == len(items).
    assert best == max(items[:i]) and i == len(items)
    return best


print("result:", largest([3, 8, 2, 9, 4]))

i=1: best=3 is the largest of [3]
i=2: best=8 is the largest of [3, 8]
i=3: best=8 is the largest of [3, 8, 2]
i=4: best=9 is the largest of [3, 8, 2, 9]
result: 9

Each line of the output comes from one pass, just after its invariant check, and the invariant held every time; the assertion after the loop checks the exit as well. max(items[:i]) makes each check cost as much as a whole pass over the list, which is fine while testing and the reason such checks do not belong in production code.

A broken loop that still passes a test

Here is the same function with an easy mistake: the loop starts at index 2 instead of 1, so the second item is never looked at.

def largest(items, check=False):
    """Meant to return the largest item, but the loop starts one place too late."""
    best = items[0]
    for i in range(2, len(items)):  # the bug: index 1 is never looked at
        if check:
            assert best == max(items[:i]), f"invariant broken at i={i}: best={best}, max(items[:{i}])={max(items[:i])}"
        if items[i] > best:
            best = items[i]
    return best


print("largest([3, 8, 2, 9]) =", largest([3, 8, 2, 9]))  # right, by luck
print("largest([3, 8, 2]) =", largest([3, 8, 2]))  # wrong: 8 is larger
largest([3, 8, 2, 9], check=True)  # the invariant check stops at the first bad step

largest([3, 8, 2, 9]) = 9
largest([3, 8, 2]) = 3

Traceback (most recent call last):
  File "largest_bug.py", line 14, in <module>
    largest([3, 8, 2, 9], check=True)  # the invariant check stops at the first bad step
    ~~~~~~~^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "largest_bug.py", line 6, in largest
    assert best == max(items[:i]), f"invariant broken at i={i}: best={best}, max(items[:{i}])={max(items[:i])}"
           ^^^^^^^^^^^^^^^^^^^^^^
AssertionError: invariant broken at i=2: best=3, max(items[:2])=8

The first call returns 9, the right answer, because the largest item happens to come late in the list. A test on [3, 8, 2, 9] alone would pass. The second call shows the bug: 3 instead of 8. With the invariant checked, the very first pass fails, at i = 2: best is still 3 while the first two items include 8. The check catches the mistake on the very input whose final answer happened to be right, because it tests every step, not only the result.

Termination: something must shrink

A loop that never stops never returns a wrong answer, and it is still not correct. To show that a loop stops, find a variant: a whole number that is never negative and gets smaller on every pass, so the loop cannot run forever. In binary search over the positions lo up to hi - 1, the variant is hi - lo, the number of positions left.

def search(items, target, buggy=False):
    """Index of target in the sorted list items, or -1. Positions lo up to hi - 1 are still to be searched."""
    lo, hi = 0, len(items)
    sizes = []
    while lo < hi:
        sizes.append(hi - lo)  # the variant: it must shrink on every pass
        if len(sizes) > 8:
            return f"no answer: hi - lo went {sizes}, the loop never ends"
        mid = (lo + hi) // 2
        if items[mid] == target:
            return f"found at {mid}: hi - lo went {sizes}"
        if items[mid] < target:
            lo = mid if buggy else mid + 1  # the bug keeps mid in the range
        else:
            hi = mid
    return f"not found: hi - lo went {sizes + [hi - lo]}"


prices = [10, 20, 30, 40]
print("correct, 35:", search(prices, 35))
print("correct, 20:", search(prices, 20))
print("buggy,   20:", search(prices, 20, buggy=True))
print("buggy,   35:", search(prices, 35, buggy=True))

correct, 35: not found: hi - lo went [4, 1, 0]
correct, 20: found at 1: hi - lo went [4, 2]
buggy,   20: found at 1: hi - lo went [4, 2]
buggy,   35: no answer: hi - lo went [4, 2, 1, 1, 1, 1, 1, 1, 1], the loop never ends

In the correct version hi - lo shrinks on every pass until the target is found or nothing is left. The buggy version sets lo = mid instead of lo = mid + 1. Once a single position is left and its value is below the target, mid is lo itself, lo = mid changes nothing, and hi - lo stays 1 forever; the example gives up after eight passes. Notice that the buggy version never returns a wrong position. When it returns at all, its answer is right.

That difference has names:

• A loop is partially correct if, whenever it stops, its result meets the postcondition.
• It is totally correct if it is partially correct and also stops on every input that meets the precondition.

Hoare’s rules on their own prove only the first: his paper says a proved result holds provided the program terminates, and calls this “conditional” correctness. The variant supplies the second.

Half-open ranges prevent off-by-one errors

Many off-by-one bugs are invariant bugs: the code means “positions lo to hi, both included” in one place and “lo up to, but not including, hi” in another. Python’s range(lo, hi) and slices such as items[lo:hi] are half-open: they include lo and exclude hi. That convention has useful properties: the length is hi - lo, an empty range is simply lo == hi, and two ranges [a, b) and [b, c) join with no gap and no overlap. Choose one convention for each loop, write it in the invariant, and keep it everywhere in that loop. The binary search above uses the half-open interval of positions from lo up to hi.

Assertions check invariants, never input

Python runs assertions only while __debug__ is true. Started with the -O option, it removes every assert statement before running the program, so a check written as an assertion silently disappears:

import subprocess
import sys

program = """
def withdraw(balance, amount):
    assert 0 < amount <= balance, "amount out of range"
    return balance - amount

print(withdraw(500, 800))
"""

for command in (["python3"], ["python3", "-O"]):
    run = subprocess.run([sys.executable, *command[1:], "-c", program], capture_output=True, text=True)
    shown = run.stdout.strip() or run.stderr.strip().splitlines()[-1]
    print(" ".join(command) + ":", shown)

python3: AssertionError: amount out of range
python3 -O: -300

Without -O, the assertion stops a withdrawal of 800 from a balance of 500. With -O, the check is gone and the balance goes to −300.

Key takeaways

• A specification is a precondition on the input and a postcondition on the result; the postcondition must pin the answer down completely.
• A loop invariant is true every time the loop test is checked. Prove it true at the start, show that each pass keeps it, and check that at the exit it gives the postcondition.
• Asserting the invariant while testing finds a broken loop on the first pass that breaks it, even when the final answer happens to be right.
• Partial correctness means “right whenever it stops”; total correctness adds “always stops”, shown with a variant that shrinks on every pass.
• Assertions vanish under python -O: use them for invariants, never to validate input.