Problems, mathematics and analysis · 04 / 53
Invariants, induction and testing
Understand → trace → implement → justify
2 min reading · allow extra time for practiceAn invariant is a proposition maintained at a specified point. Prove initialisation, preservation and the implication at termination. In insertion sort, the first i elements being sorted and preserving their multiset is a suitable invariant.
Sorted output alone is insufficient: values may have been lost or duplicated. Sortedness and permutation preservation are separate properties. Termination also matters; find a nonnegative measure that decreases. Recursive problems must shrink toward a base case.
Tests discover bugs but finite testing does not prove correctness on infinitely many inputs. Use empty, singleton, duplicate, reversed, overflow and disconnected cases. Compare optimised algorithms with a simple reference on small inputs, and check contract properties rather than only a few expected outputs.
A worked trace
Binary-search invariant: any possible target lies in [lo,hi). When lo=hi the interval is empty. Bound updates must not discard candidates.
Cost and assumptions
Proof establishes correctness, not efficiency. A correct O(n²) solution is preferable to an incorrect O(log n) one.
Executable example
Run with Python 3. Assertions check a small example; they do not constitute a general correctness proof. Some advanced examples are explicitly small models or reference oracles, not full production implementations.
from collections import Counter
def assert_sort_contract(original, result):
assert all(result[i] <= result[i+1] for i in range(len(result)-1))
assert Counter(original) == Counter(result)
assert_sort_contract([3,1,3], [1,3,3])TEST YOUR UNDERSTANDING
Your turn
Can a nonterminating loop preserve an invariant?
Reveal the reasoning
Yes. A while True loop assigning x=x preserves x≥0 but never terminates. Partial and total correctness differ.
Take it further
- Write down the input contract and the invariant before changing the example.
- Add empty, boundary, duplicate and adversarial cases where they are relevant. Compare with a simple oracle.
- Derive the cost under the stated model; measure several input sizes and explain discrepancies.
Primary reading & lecture notes
Original explanations in this course; these references provide proofs and further reading. Source links may cover the broader module.
Jeff Erickson · Algorithms ↗