FREE LESSON · Mathematics & logic · 2 OF 4
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
Maintain this invariant: if the target exists, it lies inside the current half-open interval [low, high). Comparing the midpoint removes only a region that cannot contain the target, so the invariant survives. The interval strictly shrinks, so the loop terminates. At termination the remaining state determines found versus absent.
Correctness needs both preservation and progress: staying true forever is not enough if the loop never ends.