FREE LESSON · Mathematics & logic · 2 OF 12
Software Invariants and Correctness
Claims, counterexamples, and invariants: How software earns a guarantee
A proof explains why failure has nowhere to hide.
A universal claim must survive every valid case, so one counterexample defeats it. A constructive proof shows how to produce an object. Induction handles recursively built or repeated structure. In programs, an invariant is a statement kept true before and after each step; together with termination, it turns local reasoning into an end-to-end guarantee.
Testing samples executions. Proof constrains the entire defined space, provided the model and assumptions are correct.
The loop invariant behind binary search
Assume an array sorted in ascending order. Search a half-open interval [low, high): compare the midpoint, return on equality, and otherwise discard only the region sortedness proves cannot contain the target. If the target exists, it stays in the candidate interval. The interval strictly shrinks; if it becomes empty before a match, the target is absent.
Correctness needs both preservation and progress: staying true forever is not enough if the loop never ends.
Sources and further reading
- Mathematics for Computer Science: MIT OpenCourseWare
- Book of Proof: Richard Hammack · open textbook
- Single Variable Calculus: MIT OpenCourseWare