register or is a bitfield, since you can't take the address of a bitfield or a register. The algorithm doesn't
work if a or b are of different-sized types, or if either of them points to an array.
In case anyone is not convinced and still believes that program proofs are ready for prime time,
reproduced below is a typical single verification clause from an actual program proof that is believed
correct. The clause arises in the proof of a Fourier transform (a clever kind of signal waveform
analysis), and was presented in a 1973 report, "On Programming," by Jacob Schwartz of New York
University's Courant Institute.
If you find anyone who still believes that program proving is practical, offer them this challenge. We
have made a simple change to this proof; please find it. It is possible to identify the amendment from
the information that is there. The answer is given at the end of the chapter.
A single verification condition from the proof of a Fast Fourier Transform
program
Programmer Health Warning: Don't actually study this!
The purpose of this horrible looking program proof is to convince you of the impracticality
of program proofs!
How would you like to spend your day poring over pages and pages like that? There's a substantial
probability that the mere act of reproducing the condition here has introduced errors. How could an
entire proof based on reams of conditions like these ever be written out accurately, let alone proved
for completeness, consistency, and correctness?
Some people suggest that the complicated notation can be managed by having automated program
provers. But how can we be sure that such a program prover has no bugs in it? Perhaps feed the
verifier into itself for verification? A moment's reflection reveals why that is not adequate. It's like
asking a possible liar, "Do you tell lies?" You cannot trust a denial.
Further Reading
For more detail on the problems with program verification, there's a very readable paper in
Communications of the ACM, vol. 22, no. 5, May 1979, called "Social Processes and Proofs of
Theorems and Programs," written by Richard de Millo, Richard Lipton, and Alan Perlis. It provides
the background on why program proofs are not practical now, and probably won't ever be. The
primary point that program proofs prove is that the present process of program proving is not a
practical proposition. Phew! Let's stick with the "engineering hacks" for now.
Programming Solution
Answer to Change in Program Proof