Java Reference
In-Depth Information
Furthermore, we know that
i = 0
, because the loop is terminating. But because
i = 0
,
r ß b
i
= r ß b
0
= r
. Hence
r = a
n
, and the method really does
compute the
n
th power of
a
.
This technique is quite useful, because it can explain an algorithm that is not at all
obvious. The condition (I) is called a loop invariant because it is true when the
loop is entered, at the top of each pass, and when the loop is exited. If a loop
invariant is chosen skillfully, you may be able to deduce correctness of a
computation. See [
3
] for another nice example.
R
ANDOM
F
ACT
6.2: Correctness Proofs
In Advanced Topic 6.5 we introduced the technique of loop invariants. If you
skipped that topic, have a glance at it now. That technique can be used to
rigorously prove that a loop computes exactly the value that it is supposed to
compute. Such a proof is far more valuable than any testing. No matter how many
test cases you try, you always worry whether another case that you haven't tried
yet might show a bug. A proof settles the correctness for all possible inputs.
For some time, programmers were very hopeful that proof techniques such as loop
invariants would greatly reduce the need of testing. You would prove that each
simple method is correct, and then put the proven components together and prove
that they work together as they should. Once it is proved that
main
works
correctly, no testing is required. Some researchers were so excited about these
techniques that they tried to omit the programming step altogether. The designer
would write down the program requirements, using the notation of formal logic.
An automatic prover would prove that such a program could be written and
generate the program as part of its proof.
Unfortunately, in practice these methods never worked very well. The logical
notation to describe program behavior is complex. Even simple scenarios require
many formulas. It is easy enough to express the idea that a method is supposed to
compute a
n
, but the logical formulas describing all methods in a program that
controls an airplane, for instance, would fill many pages. These formulas are
created by humans, and humans make errors when they deal with difficult and
