[bartw]

It falls so far outside of day to day programming, that it feels somewhat alien.

I however miss the argument a bit, as i can imagine a mechanical transform that can turn the premature exit version into one without. (using if statements to remove all operations until the end of the loop)

[ianferrel]

I agree that it's pretty easy to transform the code. You could also take the code block in the loop, make it a separate function, and return instead of break. It's no harder to understand a block with break statements than it is to understand a function with multiple returns, although maybe Dijkstra wasn't a big fan of multiple returns, either.

[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)