[pascal_cuoq]

Good thinking on both counts. Multiple returns are another limited form of exceptions, and you don't need to go back in time to ask the Dijkstra from that period if he disliked them. They too escaped theoretical treatment as it was formulated at that time :)

I have put some example rules to introduce exceptions in Hoare logic at http://snipt.org/lWg (I needed monospaced fonts, sorry for the inconvenience)