A loop invariant is a relation among program variables that is true when control enters a loop, remains true each time the program executes the body of the loop, and is still true when control exits the loop. Understanding loop invariants can help us analyze programs, check for errors, and derive programs from specifications.
Here is a simple example. This Java method named sum is
a function that returns the sum of the elements in array
a, its argument. It uses the local variable
s to accumulate the sum and uses i to index
the array elements.
public static int sum(int a[]) {
int s = 0;
for (int i = 0; i < a.length; i++) {
// s is the sum of the first i array elements
// s == a[0] + .. + a[i-1]
s = s + a[i];
}
return s;
}
The comments in the loop body describe the invariant. The first
comment describes the invariant in English: s is the sum
of the first i array elements. The second comment
expresses the invariant in a form similar to a Java boolean
expression: s == a[0] + .. + a[i-1]. This form emphasizes
that the invariant is an assertion, an expression that
should always evaluate to true (the two dots
.. used here to indicate the other terms in the sum are
not legal Java syntax).
The invariant expresses a relation between the three variables
s, i, and a that remains true even
when the values of s and i change:
s is always the sum of the first i
elements in a. When control enters the loop,
i is 0 so s is the sum of no
array elements. When control exits the loop, i is
a.length, so s is the sum of all of
the array elements. This is the intended result.
This simple example shows why thinking about loop invariants can help us write programs. When the program exits a loop, the loop invariant expresses the intended value(s) of the variable(s) at that point. Therefore we can work backwards from the intended values to the loop invariant, and then to the code itself. This can be a systematic method for writing programs which can supplement the usual method of relying on intuition and lots of trial-and-error. Programs derived in this way can be surprising and unobvious --- the kind that make you wonder, "How did they come up with that?"
It is necessary that the loop invariant be true on each iteration
before executing the body of the loop, and again after executing the
body. In our example, the body of the loop is the
statement s = s + a[i], followed by i++
(because the third expression in the for statement is
actually executed at the end of the body of the loop, each time the
body is executed). The first time the program executes the loop,
i == 0 and sum == 0
before executing the body, and i == 1 and sum ==
a[0] after executing the body. Both
situations satisfy the invariant.
The for loop makes it a bit difficult to see what's going
on because the statement which is actually executed at the end of the
body of the loop (i++ in our example) doesn't appear
there, it appears in the for statement itself. For the
purposes of understanding and deriving loops, it is often clearer to
express a for loop as the equivalent while loop.
Here is how to transform a for loop to the equivalent
while loop. This for loop
for (s; p; u) {
t;
}
is equivalent to this while loop
s;
while (p) {
t;
u;
}
So our example code can be transformed to
public static int sum2(int a[]) {
int s = 0, i = 0;
while (i < a.length) {
// s is the sum of the first i array elements
// s == a[0] + .. + a[i-1]
s = s + a[i];
i = i + 1;
}
return s;
}
We need a few more definitions.
The guard is the boolean expression that determines whether
to execute the body of the loop. The program executes the body of the
loop as long as the guard is true. In a
while loop, the guard is the boolean expression that
occurs in the while statement (in a for
loop, the guard is the second expression in parentheses in the
for statement). In this example, the guard is i <
a.length.
The variant is a numeric expression that measures how much work
is left to do. Usually the variant does not occur explicitly in the
code, you must infer it. Quite often the variant is simply the
number of loop iterations that remain to be done. In our example,
the variant is a.length - i.
Now we have all the concepts we need to understand loops. A loop is correct if the five conditions in this checklist are all true:
We can confirm all five conditions in our example:
i == 0 && s == 0 before entering the loop
i == 1
&& s == a[0], then i == 2 && s == a[0] + a[1],
etc.
i = i + 1 decreases the variant a.length - i.
1,
the guard i < a.length becomes false.
i == a.length
and the invariant s == a[0] + .. + a[length-1]
describe the goal.
Before we go on, let's check our understanding of invariants. For each of these code samples, see if you can express the loop invariant in English and in symbols (as a Java boolean expression, or as near to one as you can write).
This code computes the power xn by repeated multiplication:
public static int power(int x, int n) {
int p = 1, i = 0;
while (i < n) {
p = p * x;
i = i + 1;
}
return p;
}
This code performs integer division by repeated subtraction. It
divides numerator n by divisor d, returning quotient
q and also calculating remainder r. To
understand this code, it is useful to understand this definition for for
integer division that relates relates the outputs q and
r to the inputs n and d:
r < d && n = q*d + r
public static int quotient(int n, int d) {
int q = 0, r = n;
while (r >= d) {
r = r - d;
q = q + 1;
}
return q;
}
These exercises are a little contrived. As we shall see, it is usually more effective to start with the loop invariant and derive the code from that.
We can derive loops by considering the general pattern that relates
the code in the loop to the assertions. Here I is the
invariant, P is the guard, S is the code that precedes the loop and Tis the code in the body of the loop:
S
// I
while (P) {
// I
T
// I
}
// !P && I
This shows that the assertion !P && I will be true when
code exits the loop. This is called the postcondition (because
it is true after executing the loop).
Let's look again at integer division. Now we know enough to derive
the code from the definition r < d && n == q*d + r.
We want this definition to match the postcondition !P && I.
We notice that !P in the postcondition matches r < d
in the definition, and the invariant
I matches n == q*d + r.
We can derive the guard P by negating r < d
to obtain r >= d. Filling in the assertions, we now have:
S
// n == q*d + r
while (r >= d) {
// n == q*d + r
T
// n == q*d + r
}
// r < d && n == q*d + r
Now we have to derive the code fragments S and
T. The basic idea is to count how many times we can
subtract the divisor d from the numerator n.
The quotient q is the counter, and remainder
r is what remains after the subtraction.
Our first job is to write S, the startup code that
initializes q and r. S has to
establish the invariant I. It seems reasonable to start
with r = n; q = 0;. Substituting these values into
I, we obtain n == 0*d + n which is true.
Checking S against I in
this way gives us confidence that our code is correct.
Our next job is to write T, the body of the loop. T
must preserve the invariant I. It seems reasonable to try
r = r - d; q = q + 1. So, for example, after the first time
we execute the loop body we'll have r == n - d && q == 1 (why?).
Plugging these values back into I we obtain
n == 1*d + n - d which is true. And so on, each time we execute
the body of the loop. Again, checking T against I
shows that our code is correct. We have derived
r = n;
q = 0;
// n == q*d + r
while (r >= d) {
// n == q*d + r
r = r - d;
q = q + 1;
// n == q*d + r
}
// r < d && n == q*d + r
If you wish, you can use Java coding tricks to express this in a more compressed form:
for (r = n, q = 0; r >= d; q++) r -= d;
Consider the code for xn in the previous exercise.
Write the boolean expressions for the guard P and
the invariant I. Annotate the code with assertions
and confirm to your satisfaction that the assertions are correct.
A boolean expression that defines the integer square root
r of non-negative integer n is r*r <=
n && n < (r+1)*(r+1). Derive a function sqrt
that takes argument n and returns its root r
(the easiest algorithm simply counts up to r).
My favorite book on program derivation is Programming in the 1990s: An Introduction to the Calculation of Programs by Edward Cohen, Springer 1990. There are other good books by Dijkstra, Gries, and Kaldewaij.