Re-engineering Loops
S. Pan · The Computer Journal · 1996
Loops with multiple-exits and flags detract from the quality of imperative programs. They tend to make control-structures difficult to understand and, at the same time, introduce the risk of non-termination and other correctness problems. A systematic, generally applicable procedure, called loop rationalization, which removes such features and logically simplifies loop structures is presented. This method, which is founded on the principle of separation of concerns, employs strongest postcondition calculations and congruent equivalence transformations to improve loops. A by-product of the process is that it detects a range of defects such as unreachable code and a class of non-termination problems.