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.

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)