Imperative style
The following sets R = n!.
R = 1;
I = 1;
while I < n
R = I * R
I = I + 1
end
But why should we believe that it works? One method is to use
a loop invariant, which is a fact about
the values of the variables that is true each time the program gets to
the top of the loop. A loop invariant for this loop is
R = (I-1)!. The values that R and I take on
are shown in the following table. Notice that, at every line, R = (I-1)!.
R I
--- ---
1 1
1 2
2 3
6 4
24 5
...
Can we convince ourselves that the loop invariant is really true at
every line?
We can by noticing two things.
- It is true at the first line
- For each line, if the loop invariant is true at that line, then
it is also true at the next line.
It is easy to see that R = (I-1)! is true at the first
line because 0! = 1.
Imagine that we reach
a row where R = x and I = y. The next line will have
R = xy and I = y+1.
R I
--- ---
x y
yx y+1
If we believe that x = (y-1)!, why should we
believe that yx = ((y+1)-1)!?
Since we are
presuming that x = (y-1)!, we can replace x
by (y-1)! in the equation
yx = ((y+1)-1)!, yielding the fact that we need to
be true:
y(y-1)! = ((y+1)-1)!
or
(y-1)!y = y!
This fact is the basis for our reasoning that our program works.
It is implicit, not stated in the program, but it is key to
the program's correctness.
|