REENGINEERING LOOPS

Loops with multiple-exits and flags detract from the quality of impera tive programs. They tend to make control-structures difficult to under stand and, at the same time, introduce the risk of non-termination and other correctness problems. A systematic, generally applicable proced ure, called loop rationalization, which removes such features and logi cally simplifies loop structures is presented. This method, which is f ounded on the principle of separation of concerns, employs strongest p ostcondition calculations and congruent equivalence transformations to improve loops, A byproduct of the process is that it detects a range of defects such as unreachable code and a class of non termination pro blems.