Expert C Programming

The problem with program verifiers is that they cheat on toy problems in order to get results.

—Anonymous

Readers of the Usenet network's C language forum were somewhat surprised to see the following
strident posting one summer day. The poster (name omitted to protect the guilty) demanded the
universal adoption of formal program proofs, because "anything else is just engineering hacks." His
argument included a 45-line proof of the correctness of a three-line C program. In the interests of
brevity I've condensed the posting somewhat.

Table 10-3. Program Proofs Posting

From: A proponent of program proofs

Date: Fri May 15 1991, 12:43:52 PDT

Subject: Re: Swapping 2 values without a temporary.

Someone asks if the following program fragment (to swap 2 values) works:

a ^= b; / Do 3 successive XORs /

b ^= a;

a ^= b;

Here's the answer.

Make the Standard Assumptions that (1) this sequence executes atomically, and

(2) it executes without hardware failure, memory limitations or math failure.

Then after the sequence

a ^= b; b ^= a; a ^= b;

*a, and *b will have the values f3(a), and f3(b) where:

f3 = lambda x.(x == a? f2(a) ^ f2(b): f2(x))

f2 = lambda x.(x == b? f1(b) ^ f1(a): f1(x))

f1 = lambda x.(x == a? a ^ b: *x)

or in more readable terms:

f3(a) = f2(a) ^ f2(b), f3(x) = f2(x) else

f2(b) = f1(b) ^ f1(a), f2(x) = f1(x) else

f1(a) = a ^ b, f1(x) = *x else