Reengineering Loops

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 simplifies loop structures is presented. This method, which is founded on the principle of separation of concerns, is based on strongest postcondition calculations and congruent equivalence transformations. Not only does this method logically simplify loop structures; it also detects a range of defects including a class of non-termination problems and unreachable code. 1