Editing Loop invariant (section)

{{Short description|Invariants used to prove properties of loops}}
{{for|the computer programming  optimization technique|Loop-invariant code motion}}

In [[computer science]], a '''loop invariant''' is a property of a [[Computer program|program]] [[Control flow#Loops|loop]] that is true before (and after) each iteration. It is a [[logical assertion]], sometimes checked with a code [[Assertion (software development)|assertion]]. Knowing its invariant(s) is essential in understanding the effect of a loop.

In [[formal verification|formal program verification]], particularly the [[Hoare logic|Floyd-Hoare approach]], loop invariants are expressed by formal [[predicate logic]] and used to prove properties of loops and by extension [[algorithm]]s that employ loops (usually [[Correctness (computer science)|correctness]] properties).
The loop invariants will be true on entry into a loop and following each iteration, so that on exit from the loop both the loop invariants and the loop termination condition can be guaranteed.

From a programming methodology viewpoint, the loop invariant can be viewed as a more abstract specification of the loop, which characterizes the deeper purpose of the loop beyond the details of this implementation. A survey article <ref>Carlo A. Furia, [[Bertrand Meyer]] and Sergey Velder. "Loop invariants: analysis, classification, and examples."ACM Computing Surveys.  vol. 46, no. 3, February 2014([http://se.ethz.ch/~meyer/publications/methodology/invariants.pdf]</ref> covers fundamental algorithms from many areas of computer science (searching, sorting, optimization, arithmetic etc.), characterizing each of them from the viewpoint of its invariant.

Because of the similarity of loops and [[recursion|recursive]] programs, proving partial correctness of loops with invariants is very similar to proving the correctness of recursive programs via [[structural induction|induction]].  In fact, the loop invariant is often the same as the inductive hypothesis to be proved for a recursive program equivalent to a given loop.