Loop Invariants¶

Identifying properties that remain true throughout iterative execution enables reasoning about correctness without tracing every iteration; invariants bridge the gap between individual steps and final outcomes.

Tension Addressed¶

Optimality vs. Simplicity (systematic correctness reasoning)

Recognizable As¶

Comments stating "at this point, X is always true," assertions in loops, inductive proof structure, sorted-prefix in sorting algorithms, partial result validity

Canonical Sources¶

Floyd, Assigning Meanings to Programs (1967); Hoare, An Axiomatic Basis for Computer Programming (1969)

Transfers To¶

Contract programming, formal verification, database transaction guarantees, protocol design, state machine correctness

Loop invariants are the bridge between operational (step-by-step) and denotational (what it computes) understanding of algorithms.