A formal basis for removing goto statements

Abstract

Goto statements detract from the quality of imperative programs. They tend to make controlstructures difficult to understand and, at the same time, introduce the risk of non-termination and other correctness problems. A new, formal, generally applicable procedure for removing all goto statements from program structures is presented. This method is based on formal semantics and congruent equivalence transformations. Not only does the method logically simplify program structures; it also detects a range of defects including a class of non-termination problems, unreachable code and redundancy problems. The method can also be used to eliminate recursion.