I know that the article is foremost about Dijkstra, and uses Hoare-style verification of programs as an example only, but there's a C function with "break;" being verified using Hoare logic right there:

http://frama-c.cea.fr/jessie_tutorial_index.html

Presumably exceptions were not a standard feature in programming languages when Dijkstra made his comment about premature-loop-exits. The "break;" C construct is only a restricted form of exception and exceptions are much better understood now than then. Verifying a program that uses them is no more difficult than verifying a program that doesn't.

Pascal Cuoq