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

Posted on November 4, 2011 by Tommy McGuire
Labels: theory, notation, link, Knuth, Dijkstra, programming language

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.

active directory applied formal logic ashurbanipal authentication books c c++ comics conference continuations coq data structure digital humanities Dijkstra eclipse virgo electronics emacs goodreads haskell http java job Knuth ldap link linux lisp math naming nimrod notation OpenAM osgi parsing pony programming language protocols python quote quotes R random REST ruby rust SAML scala scheme shell software development system administration theory tip toy problems unix vmware yeti
Member of The Internet Defense League
Site proudly generated by Hakyll.