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

Posted on November 4, 2011 by Tommy McGuire

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. Site proudly generated by Hakyll.