On the Translation of Procedures to Finite Machines

Abstraction Allows a Clean Proof
  • Markus Müller-Olm
  • Andreas Wolf
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1782)


We prove the correctness of the translation of a prototypic While-language with nested, parameterless procedures to an abstract assembler language with finite stacks. A variant of the well-known wp and wlp predicate transformers, the weakest relative precondition transformer wrp, together with a symbolic approach for describing semantics of assembler code allows us to explore assembler programs in a manageable way and to ban finiteness from the scene early.


compiler correctness refinement resource-limitation predicate transformer procedure verification 


  1. 1.
    E. Börger and I. Durdanović. Correctness of compiling Occam to transputer code. The Computer Journal, 39(1), 1996.Google Scholar
  2. 2.
    L. M. Chirica and D. F. Martin. Towards compiler implementation correctness proofs. ACM TOPLAS, 8(2):185–214, April 1986.zbMATHCrossRefGoogle Scholar
  3. 3.
    E. W. Dijkstra and C. S. Scholten. Predicate Calculus and Program Semantics. Texts and Monographs in Computer Science. Springer-Verlag, 1990.Google Scholar
  4. 4.
    J. D. Guttman, J. D. Ramsdell, and M. Wand. VLISP: A verified implementation of Scheme. Lisp and Symbolic Computation, 8:5–32, 1995.CrossRefGoogle Scholar
  5. 5.
    C. A. R. Hoare, I. J. Hayes, H. Jifeng, C. C. Morgan, A. W. Roscoe, J. W. Sanders, I. H. Sorenson, J. M. Spivey, and B. A. Sufrin. Laws of programming. Communications of the ACM, 30(8):672–687, August 1987.zbMATHCrossRefGoogle Scholar
  6. 6.
    C. A. R. Hoare, H. Jifeng, and A. Sampaio. Normal form approach to compiler design. Acta Informatica, 30:701–739, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    H. Langmaack. Software engineering for certification of systems: specification, implementation, and compiler correctness (in German). Informationstechnik und Technische Informatik, 39(3):41–47, 1997.Google Scholar
  8. 8.
    J. S. Moore. Piton, A Mechanically Verified Assembly-Level Language. Kluwer Academic Publishers, 1996.Google Scholar
  9. 9.
    M. Müller-Olm. Modular Compiler Verfication: A Refinement-Algebraic Approach Advocating Stepwise Abstraction, LNCS 1283. Springer-Verlag, 1997.Google Scholar
  10. 10.
    M. Müller-Olm and A. Wolf. On excusable and inexcusable failures: towards an adequate notion of translation correctness. In FM’ 99, LNCS 1709, pp. 1107–1127. Springer-Verlag, 1999.Google Scholar
  11. 11.
    H. R. Nielson and F. Nielson. Semantics with Applications: A Formal Introduction. Wiley, 1992.Google Scholar
  12. 12.
    T. S. Norvell. Machine code programs are predicates too. In 6th Refinement Workshop, Workshops in Computing. Springer-Verlag and British Computer Society, 1994.Google Scholar
  13. 13.
    E. Pofahl. Methods used for inspecting safety relevant software. In High Integrity Programmable Electronics, pages 13–14. Dagstuhl-Sem.-Rep. 107, 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Markus Müller-Olm
    • 1
  • Andreas Wolf
    • 2
  1. 1.Fachbereich InformatikUniversität DortmundDortmundGermany
  2. 2.Institut für Informatik und Praktische MathematikChristian-Albrechts-UniversitätKielGermany

Personalised recommendations