A **loop invariant** is a property or condition that holds true before and after each iteration of a loop in a computer program. It is used primarily in the context of program correctness and formal verification to help understand and prove that a loop behaves as intended. The concept of a loop invariant is important in analyzing loops for correctness, particularly when applying proofs by induction.
Articles by others on the same topic
A statement true whenever execution reaches a chosen point in a loop, usually immediately before its condition is tested. Establish it initially, preserve it through each iteration, and combine it with the exit condition to establish algorithm correctness. Termination needs a separate argument.[ref]
Loop invariants. CS 2112 Fall 2019; Loop invariants, Using loop invariants to show code is correct: the three partial-correctness obligations and separate Termination step
Write for the loop invariant, for the condition, for the precondition, and for the postcondition. Prove that initialization under establishes , that a completed body starting with and restores , and that with false implies .[ref]
Loop invariants. CS 2112 Fall 2019; Loop invariants, Using loop invariants to show code is correct: Establishment, Preservation, and Postcondition
In the prefix maximum correctness example, the loop invariant remembers exactly the maximum of the processed prefix and the valid index bounds. The weaker statement survives every iteration, but does not imply the postcondition: for , the wrong value satisfies it. A useful loop invariant retains enough information to recover the answer when the condition becomes false.