A FORMAL BASIS FOR REMOVING GOTO STATEMENTS

Goto statements detract from the quality of imperative programs. They tend to make control-structures difficult to understand and, at the sa me time, introduce the risk of non-termination and other correctness p roblems. A new, formal, generally applicable procedure for removing al l 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 als o detects a range of defects including a class of non-termination prob lems, unreachable code and redundancy problems. The method can also be used to eliminate recursion.