Goto elimination in program algebra

This paper shows that program algebra (PGA) [J.A. Bergstra, M.E. Loots, Program algebra for sequential code, J. Logic Algebraic Programm. 51 (2002) 125–156] offers a mathematical and systematic framework for reasoning about correctness and equivalence of algorithms and transformation rules for goto removal. We study correctness and equivalence for the algorithm proposed by Cooper for goto elimination with additional boolean variables. To remove goto statements without the use of additional variables, we propose a technique to get rid of head-to-head crossings and subsequently employ the results of Peterson et al. and Ramshaw. Finally, we provide formal correctness proofs in the setting of PGA for industrial transformation rules given recently by Veerman for restructuring Cobol programs in real-life applications. We hereby show that PGA can explain goto elimination with mathematical rigor to a larger public.