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]
Articles by others on the same topic
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.