Loop invariant

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.