The nature of loops in programming

Bertrand Meyer

In program semantics and verification, reasoning about loops is complicated by the need to produce two separate mathematical arguments: an invariant, for functional properties (ign…