- Goto elimination in program algebra
- Science of Computer Programming
- Volume | Issue number
- 73 | 2-3
- Pages (from-to)
- Document type
- Faculty of Science (FNWI)
- Informatics Institute (IVI)
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.
- go to publisher's site
If you believe that digital publication of certain material infringes any of your rights or (privacy) interests, please let the Library know, stating your reasons. In case of a legitimate complaint, the Library will make the material inaccessible and/or remove it from the website. Please Ask the Library, or send a letter to: Library of the University of Amsterdam, Secretariat, Singel 425, 1012 WP Amsterdam, The Netherlands. You will be contacted as soon as possible.