Loop invariant

In computer science, a loop invariant is a property of a program loop that is true before (and after) each iteration. It is a logical assertion, sometimes checked within the code by an assertion call. Knowing its invariant(s) is essential in understanding the effect of a loop.

In formal program verification, particularly the Floyd-Hoare approach, loop invariants are expressed by formal predicate logic and used to prove properties of loops and by extension algorithms that employ loops (usually 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.

Because of the similarity of loops and recursive programs, proving partial correctness of loops with invariants is very similar to proving correctness of recursive programs via 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.

Loop-invariant code motion, which involves moving code out of the loop if that does not change the effect of the program, is not directly related to loop invariants, which are properties of the loop overall.

Informal example

The following C subroutine max() returns the maximum value in its argument array a[], provided its length n is at least 1. Comments are provided at lines 3, 6, 9, 11, and 13. Each comment makes an assertion about the values of one or more variables at that stage of the function. The highlighted assertions within the loop body, at the beginning and end of the loop (lines 6 and 11), are exactly the same. They thus describe an invariant property of the loop. When line 13 is reached, this invariant still holds, and it is known that the loop condition i!=n from line 5 has become false. Both properties together imply that m equals the maximum value in a[0...n-1], that is, that the correct value is returned from line 14.

int max(int n,const int a[]) {
    int m = a[0];
    // m equals the maximum value in a[0...0]
    int i = 1;
    while (i != n) {
        // m equals the maximum value in a[0...i-1]
        if (m < a[i])
            m = a[i];
        // m equals the maximum value in a[0...i]
        ++i;
        // m equals the maximum value in a[0...i-1]
    }
    // m equals the maximum value in a[0...i-1], and i==n
    return m;
}

Following a defensive programming paradigm, the loop condition i!=n in line 5 should better be modified to i<n, in order to avoid endless looping for illegitimate negative values of n. While this change in code intuitively shouldn't make a difference, the reasoning leading to its correctness becomes somewhat more complicated, since then only i>=n is known in line 13. In order to obtain that also i<=n holds, that condition has to be included into the loop invariant. It is easy to see that i<=n, too, is an invariant of the loop, since i<n in line 6 can be obtained from the (modified) loop condition in line 5, and hence i<=n holds in line 11 after i has been incremented in line 10. However, when loop invariants have to be manually provided for formal program verification, such intuitively too obvious properties like i<=n are often overlooked.

Floyd–Hoare logic

Specifically in Floyd–Hoare logic,^[1]^[2] the partial correctness of a while loop is governed by the following rule of inference:

{\frac {\{C\land I\}\;\mathrm {body} \;\{I\}}{\{I\}\;\mathbf {while} \ (C)\ \mathrm {body} \;\{\lnot C\land I\}}}

This means:

A while loop does not have the side effect of falsifying $I$ —if the loop's body does not change an invariant $I$ from true to false given the condition $C$ , then $I$ will still be true after the loop has run as long as it was true before.
$while(C)...$ runs as long as the condition $C$ is true—after the loop has run, if it terminates, $C$ is false.

The rule above is a deductive step that has as its premise the Hoare triple $\{C\land I\}\;\mathrm {body} \;\{I\}$ . This triple is actually a relation on machine states. It holds whenever starting from a state in which the boolean expression $C\land I$ is true and successfully executing some program called body, the machine ends up in a state in which $I$ is true. If this relation can be proven, the rule then allows us to conclude that successful execution of the program while (C) body will lead from a state in which $I$ is true to a state in which $\lnot C\land I$ holds. The boolean formula I in this rule is known as the loop invariant.

The following example illustrates how this rule works. Consider the program

while (x < 10)
    x := x+1;

One can then prove the following Hoare triple:

\{x\leq 10\}\;\mathbf {while} \ (x<10)\ x:=x+1\;\{x=10\}

The condition C of the while loop is $x<10$ . A useful loop invariant I is $x\leq 10$ . Under these assumptions it is possible to prove the following Hoare triple:

\{x<10\land x\leq 10\}\;x:=x+1\;\{x\leq 10\}

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 $x<10\land x\leq 10$ is true, which means simply that $x<10$ is true. The computation adds 1 to x, which means that $x\leq 10$ is still true (for integer x).

Under this premise, the rule for while loops permits the following conclusion:

\{x\leq 10\}\;\mathbf {while} \ (x<10)\ x:=x+1\;\{\lnot (x<10)\land x\leq 10\}

However, the post-condition $\lnot (x<10)\land x\leq 10$ (x is less than or equal to 10, but it is not less than 10) is logically equivalent to $x=10$ , which is what we wanted to show.

The loop invariant plays an important role in the intuitive argument for soundness of the Floyd-Hoare rule for while loops. The loop invariant has to be true before each iteration of the loop body, and also after each iteration of the loop body. Since a while loop is precisely the repeated iteration of the loop body, it follows that if the invariant is true before entering the loop, it must also be true after exiting the loop.

Programming language support

Eiffel

The Eiffel programming language provides native support for loop invariants.^[3] A loop invariant is expressed with the same syntax used for a class invariant. In the sample below, the loop invariant expression x <= 10 must be true following the loop initialization, and after each execution of the loop body; this is checked at runtime.

    from
        x := 0
    invariant
        x <= 10
    until
        x > 10
    loop
        x := x + 1
    end

Whiley

The Whiley programming language also provides first-class support for loop invariants.^[4] Loop invariants are expressed using one or more where clauses, as the following illustrates:

function max(int[] items) -> (int r)
// Requires at least one element to compute max
requires |items| > 0
// (1) Result is not smaller than any element
ensures all { i in 0..|items| | items[i] <= r }
// (2) Result matches at least one element
ensures some { i in 0..|items| | items[i] == r }:
    //
    nat i = 1
    int m = items[0]
    //
    while i < |items|
    // (1) No item seen so far is larger than m
    where all { k in 0..i | items[k] <= m }
    // (2) One or more items seen so far matches m
    where some { k in 0..i | items[k] == m }:
        if items[i] > m:
            m = items[i]
        i = i + 1
    //
    return m

The max() function determines the largest element in an integer array. For this to be defined, the array must contain at least one element. The postconditions of max() require that the returned value is: (1) not smaller than any element; and, (2) that it matches at least one element. The loop invariant is defined inductively through two where clauses, each of which corresponds to a clause in the postcondition. 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.

Use of loop invariants

A loop invariant can serve one of the following purposes:

purely documentary
to be checked within in the code by an assertion call
to be verified based on the Floyd-Hoare approach

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. Often, run-time checking can be switched on (for debugging runs) and off (for production runs) by a compiler or a runtime option.^{[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. However, this approach is limited to very simple invariants (such as 0<=i && i<=n && i%2==0).

Distinction from loop-invariant code

A loop invariant (loop-invariant property) is to be distinguished from loop-invariant code; note "loop invariant" (noun) versus "loop-invariant" (adjective). Loop-invariant code consists of statements or expressions that can be moved outside the body of a loop without affecting the semantics of a program; 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

for (int i=0; i<n; ++i) {
    x = y+z;
    a[i] = 6*i + x*x;
}

where the calculations x = y+z and x*x can be moved before the loop, resulting in an equivalent, but faster, program:

x = y+z;
t1 = x*x;
for (int i=0; i<n; ++i) {
    a[i] = 6*i + t1;
}

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".

Loop-invariant code may induce a corresponding loop-invariant property.^{[clarification needed]} For the above example, the easiest way to see it is to consider a program where the loop invariant code is computed both before and within the loop:

x1 = y+z;
t1 = x1*x1;
for (int i=0; i<n; ++i) {
    x2 = y+z;
    a[i] = 6*i + t1;
}

A loop-invariant property of this code is (x1==x2 && t1==x2*x2) || i==0, indicating that the values computed before the loop agree with those computed within (except before the first iteration).^{[citation needed]}

References

^ R. W. Floyd. "Assigning meanings to programs." Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19–31. 1967. ([1])
^ Hoare, C. A. R. (October 1969). "An axiomatic basis for computer programming" (PDF). Communications of the ACM. 12 (10): 576–580. doi:10.1145/363235.363259. Archived from the original (PDF) on 2016-03-04. {{cite journal}}: Unknown parameter |deadurl= ignored (|url-status= suggested) (help)
^ Meyer, Bertrand, Eiffel: The Language, Prentice Hall, 1991, pp. 129–131.
^ "Designing a Verifying Compiler: Lessons Learned from Developing Whiley". Science of Computer Programming. 113: 191–220. doi:10.1016/j.scico.2015.09.006.