Expert C Programming

(provided that *a and *b are defined, i.e. a != NULL, b != NULL).

This leads to only two solutions (derived by beta reduction), namely:

if a and b are the same: f3(a) = f3(b) = 0

if a and b are different: f3(a) = b, f3(b) = a.

And about reliable verification and debugging:

mathematical verification and proof is the only reliable technique.

Everything else is engineering hacks. And contrary to the commonly

received myth, all of C is easily tractable in this way by

mathematical analysis.

Alert readers were even more startled to see the same poster follow up a few minutes later...

Table 10-4. Program Proofs Follow-Up Posting

From: A proponent of program proofs

Date: Fri May 15 1991, 13:07:34 PDT

Subject: Re: Swapping 2 values without a temporary.

Where I previously wrote:

This leads to only two solutions (derived by beta reduction),

namely:

if a and b are the same: f3(a) = f3(b) = 0

if a and b are different: f3(a) = b, f3(b) = a.

I actually meant to write

f3(a) = b, and f3(b) = a...

Not only did the proof have two errors, but the C program that he "verified" was not in fact correct to
start with! It is a quite well known result in C that it is impossible to swap two values (in the general
case) without the use of a temporary. In this case, if a and b point to overlapping objects, the algorithm
fails. Additionally, the algorithm can't even be applied if one of the values to be swapped is in a