There is also a Java version of this lecture.
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 Perl subroutine named sum is
a function that returns the sum of the elements in array
@_, its argument. It uses the local variable
$s to accumulate the sum and uses $i to index
the array elements.
sub sum {
for ($i = 0; $i < @_; $i++) {
# $s is the sum of the first $i array elements
# $s == $_[0] + .. + $_[$i-1]
$s = $s + $_[$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 Perl Boolean
expression: $s == $_[0] + .. + $_[$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 Perl syntax).
The invariant expresses a relation between the three variables
$s, $i, and @_ that remains true even
when the values of $s and $i change:
$s is always the sum of the first $i
elements in @_. When control enters the loop,
$i is 0 so $s is the sum of no
array elements. When control exits the loop, $i is
the length of @_, 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 + $_[$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 $s == 0
before executing the body, and $i == 1 and $s ==
$_[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
sub sum2 {
my $i = 0; my $s = 0;
while ($i < @_) {
# $s is the sum of the first $i array elements
# $s == $_[0] + .. + $_[$i-1]
$s = $s + $_[$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 < @_.
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 @_ - $i (the number of elements following
$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 == $_[0], then $i == 2 && $s == $_[0] + $_[1],
etc.
$i = $i + 1 decreases the variant @_ - $i.
1,
the guard $i < @_ becomes false.
$i == @_
and the invariant $s == $_[0] + .. + $_[@_-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 Perl boolean expression, or as near to one as you can write).
This code computes the power
xn (that is, x**n)
by repeated multiplication:
sub power{
my $x = shift; my $n = shift;
my $p = 1; my $i = 0;
while ($i < $n) {
$p = $p * $x;
$i = $i + 1;
}
return $p;
}
The following code
performs integer division by repeated subtraction. It
divides numerator $n by divisor $d,
returning the integer quotient
$q and also calculating remainder $r.
If the numerator is 4 and the divisor is 2, the quotient is 2;
moreover, if the numerator is 5 and the divisor is 2, the quotient is 2 also.
To understand this code, it is useful to understand this definition for
integer division that relates relates the outputs $q and
$r to the inputs $n and $d:
$r < $d && $n = $q*$d + $r
sub quotient {
my $n = shift; my $d = shift;
my $q = 0, my $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 my $r = $n; my $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
my $r = $n; my $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 Perl 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 (that is, x**n)
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).
sub bsearch {
my ($x, $a) = @_; # search for x in array a
my ($l, $u) = (0, @$a - 1); # lower, upper end of search interval
my $i; # index of probe
while ($l <= $u) {
# Loop invariant:
# if $x is in @$a, index of $x must be in the range $l .. $u
$i = int(($l + $u)/2);
# now $i is also in the range $l .. $u, it might be index of $x
print($i, "\n");
if ($a->[$i] < $x) {
# Assertion:
# index of $x must be in the range $i+1 .. $u
$l = $i+1; # make progress
}
elsif ($a->[$i] > $x) {
# Assertion:
# index of $x must be in the range $l .. $i-1
$u = $i-1; # make progress
}
else {
# Assertion:
# index of $x is $i
return $i; # found
}
}
# if $x is in @$a, it must be in the range $l .. $u, but $l > $u
# so $x must not be in @$a at all
return -1; # not found
}
Here is the maximum section sum
annotated with its invariant.
sub bentley4 { # @_ is Bentley's array X
my ($maxsofar, $maxendinghere);
for ($i = 0; $i < @_; $i++) {
# Loop invariant:
# maxsofar is max. section sum anywhere in array up to $i
# maxendinghere is max. section sum in array, where section ends at $i
$maxendinghere = max(0.0, $maxendinghere + $_[$i]);
$maxsofar = max($maxsofar, $maxendinghere);
}
return $maxsofar;
}
Bentley derives binary search using invariants and assertions in Writing Correct Programs, Communications of the ACM 26(12) 1040 - 1045, Dec. 1983, also in Programming Pearls, Addison-Wesley, Chapter 4 (both editions, 1986 and 2000). Here are Bentley's notes (PS, PDF).
My favorite book on program derivation is Programming in the 1990s: An Introduction to the Calculation of Programs by Edward Cohen, Springer 1990. Cohen derives the maximum section sum in section 10.5. There are other good books by Dijkstra, Gries, and Kaldewaij.