Knowing its invariant(s) is essential in understanding the effect of a loop.
A survey article [1] covers fundamental algorithms from many areas of computer science (searching, sorting, optimization, arithmetic etc.
Because of the similarity of loops and recursive programs, proving partial correctness of loops with invariants is very similar to proving the correctness of recursive programs via induction.
The following C subroutine max() returns the maximum value in its argument array a[], provided its length n is at least 1.
Each comment makes an assertion about the values of one or more variables at that stage of the function.
Following a defensive programming paradigm, the loop condition i!=n in line 5 should better be modified to i
In order to obtain that also i<=n holds, that condition has to be included into the loop invariant.
However, when loop invariants have to be manually provided for formal program verification, such intuitively too obvious properties like i<=n are often overlooked.
In Floyd–Hoare logic,[2][3] the partial correctness of a while loop is governed by the following rule of inference: This means: In other words: The rule above is a deductive step that has as its premise the Hoare triple
If this relation can be proven, the rule then allows us to conclude that successful execution of the program
With some variations in the notation used, and with the premise that the loop halts, this rule is also known as the Invariant Relation Theorem.
[4][5] As one 1970s textbook presents it in a way meant to be accessible to student programmers:[4] Let the notation P { seq } Q mean that if P is true before the sequence of statements seq run, then Q is true after it.
Then the invariant relation theorem holds that The following example illustrates how this rule works.
Under these assumptions it is possible to prove the following Hoare triple: While this triple can be derived formally from the rules of Floyd-Hoare logic governing assignment, it is also intuitively justified: Computation starts in a state where
The Eiffel programming language provides native support for loop invariants.
The Whiley programming language also provides first-class support for loop invariants.
[7] Loop invariants are expressed using one or more where clauses, as the following illustrates: The max() function determines the largest element in an integer array.
The fundamental difference is that each clause of the loop invariant identifies the result as being correct up to the current element i, whilst the postconditions identify the result as being correct for all elements.
A loop invariant can serve one of the following purposes: For 1., a natural language comment (like // m equals the maximum value in a[0...i-1] in the above example) is sufficient.
For 2., programming language support is required, such as the C library assert.h, or the above-shown invariant clause in Eiffel.
[citation needed] For 3., some tools exist to support mathematical proofs, usually based on the above-shown Floyd–Hoare rule, that a given loop code in fact satisfies a given (set of) loop invariant(s).
The technique of abstract interpretation can be used to detect loop invariant of given code automatically.
Loop-invariant code consists of statements or expressions that can be moved outside a loop body without affecting the program semantics.
Such transformations, called loop-invariant code motion, are performed by some compilers to optimize programs.
A loop-invariant code example (in the C programming language) is where the calculations x = y+z and x*x can be moved before the loop, resulting in an equivalent, but faster, program: In contrast, e.g. the property 0<=i && i<=n is a loop invariant for both the original and the optimized program, but is not part of the code, hence it doesn't make sense to speak of "moving it out of the loop".