Editing Control flow (section)

=== Loop variants and invariants ===
[[Loop variant]]s and [[loop invariant]]s are used to express correctness of loops.<ref>{{cite book| last=Meyer| first=Bertrand| title=Eiffel: The Language| year=1991| publisher=Prentice Hall|pages=129–131}}</ref>

In practical terms, a loop variant is an integer expression which has an initial non-negative value. The variant's value must decrease during each loop iteration but must never become negative during the correct execution of the loop. Loop variants are used to guarantee that loops will terminate.

A loop invariant is an assertion which must be true before the first loop iteration and remain true after each iteration. This implies that when a loop terminates correctly, both the exit condition and the loop invariant are satisfied. Loop invariants are used to monitor specific properties of a loop during successive iterations.

Some programming languages, such as [[Eiffel (programming language)|Eiffel]] contain native support for loop variants and invariants. In other cases, support is an add-on, such as the [[Java Modeling Language]]'s specification for [http://www.eecs.ucf.edu/~leavens/JML//jmlrefman/jmlrefman_12.html#SEC168 loop statements] in [[Java (programming language)|Java]].