Link o' the day: Donald Knuth, Tony Hoare, and goto

Hah! I found it!

Ok, I suspect I've found (and possibly blogged about) this before, but I like it, I think it is important and in any case, I just found it (again).

Following Edsger Dijkstra's Goto statement considered harmful [PDF], Donald Knuth wrote Structured programming with go to statements, in which is written (p. 289):

Axiomatics of Jumps

[...]

Just recently, however, Hoare has shown that there is, in fact, a rather simple way to give an axiomatic definition of go to statements; indeed, he wishes quite frankly that it hadn't been quite so simple. For each label \(L\) in a program, the programmer should state a logical assertion \(\alpha(L)\) which is to be true whenever we reach \(L\). Then the axioms \[ \{\alpha(L)\}\ \textbf{go to}\ L\ \{false\} \] plus the rules of inference \[ \{\alpha(L)\}\ S\ \{P\}\ \vdash\ \{\alpha(L)\}\ L:S\ \{P\} \] are allowed in program proofs, and all properties of labels and go to's will follow if the \(\alpha(L)\) are selected intelligently. One must, of course, carry out the entire proof using the same assertion \(\alpha(L)\) for each appearance of the label \(L\), and some choices of assertions will lead to more powerful results than others.

Informally, \(\alpha(L)\) represents the desired state of affairs at label \(L\); this definition says essentially that a program is correct if \(\alpha(L)\) holds at \(L\) and before all "go to \(L\)" statements, and that control never "falls through" a go to statement to the following text. Stating the assertions \(\alpha(L)\) is analogous to formulating loop invariants. Thus, it is not difficult to deal formally with tortuous program structure if it turns out to be necessary; all we need to know is the "meaning" of each label.

Unfortunately, Knuth does not cite where Hoare had just recently shown that.