A Formal Basis For Removing Goto Statements
S. Pan · The Computer Journal · 1996
Goto statements 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 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.