Correctness and Invariants

Learning objectives

• Express an algorithm as a contract.
• Use initialization, maintenance, and termination to justify a loop.
• Distinguish partial correctness from termination.

Contracts

A precondition describes valid inputs. A postcondition describes the required output. For a method that returns the maximum element:

• precondition: the sequence is non-empty;
• postcondition: the returned value belongs to the sequence and is greater than or equal to every element in it.

An algorithm is partially correct if its postcondition holds whenever it terminates. It is totally correct if it is partially correct and terminates for every input satisfying its precondition.

A loop invariant

Consider this method:

static int maximum(int[] values) {
    if (values.length == 0) {
        throw new IllegalArgumentException("values must not be empty");
    }

    int best = values[0];
    for (int i = 1; i < values.length; i++) {
        if (values[i] > best) {
            best = values[i];
        }
    }
    return best;
}

At the start of each iteration with index i, use the invariant:

best is the maximum of values[0..i).

Initialization: before the first iteration, [0, 1) contains only values[0], so the invariant holds.

Maintenance: comparing values[i] with best produces the maximum of the old prefix plus the new element. The invariant therefore holds for the next prefix.

Termination: when i == values.length, the prefix is the entire array, so the invariant implies the postcondition.

The loop terminates because i increases and is bounded above by the finite array length. The variant values.length - i is a non-negative integer that strictly decreases.

Common proof patterns

Construct	Typical argument
Sequential composition	The first postcondition establishes the second precondition
Loop	Invariant plus a decreasing variant
Recursion	Base case plus an inductive hypothesis on smaller inputs
Greedy method	Exchange argument or stays-ahead argument
Dynamic programming	Induction over the dependency order of subproblems

Exercises

1. State a useful invariant for insertion sort.
2. Explain why “the tests pass” is evidence, but not a proof for all inputs.
3. Give a partial-correctness argument for a loop that may never terminate.

References

See Cormen et al. and Hoare in the bibliography.