These classic-era structured programmers really loved their sentinels and really hated their gotos/breaks/returns. You can't tell me that it's easier to prove the correctness of this with Hoare-Dijkstra-style assertions than if you had an early return; assertions flow across control flow edges just fine, and when you have multiple control flow predecessors your precondition is the logical disjunction of those in-flowing assertions. Bob Floyd used Hoare-style triples for flow charts before Hoare.