Abstract
The classical concepts of partial and total correctness identify all types of runtime errors and divergence. We argue that the associated notions of translation correctness cannot cope adequately with practical questions like optimizations and finiteness of machines. As a step towards a solution we propose more fine-grained correctness notions, which are parameterized in sets of acceptable failure outcomes, and study a corresponding family of predicate transformers that generalize the well-known wp and wlp transformers. We also discuss the utility of the resulting setup for answering compiler correctness questions.
Acknowledgments
We are grateful to our colleagues from the ProCoS and Verifix project for many discussions that shaped our view of compiler correctness and verification; a special thank goes to Hans Langmaack for encouraging us to write this paper. The funny example of the MODULA 2 loop was communicated by Gerhard Goos.We also thank Jens Knoop, Hans Langmaack, and an anonymous referee of FMM’99 for comments that helped to improve on a draft version.
The work of the second author is supported by DFG grant La 426/15-1,2.
Chapter PDF
Similar content being viewed by others
References
A. V. Aho, R. Sethi, and J. D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1986.
K.-R. Apt and E.-R. Olderog. Verification of Sequential and Concurrent Programs. Springer-Verlag, 2nd edition, 1997.
R.-J. Back and J. von Wright. Refinement Calculus: A Systematic Introduction. Springer, 1998.
E. Bürger and I. Durdanović. Correctness of compiling Occam to transputer code. The Computer Journal, 39(1), 1996.
J. P. Bowen et al. A ProCoS II project description: ESPRIT Basic Research project 7071. Bulletin of the EATCS, 50:128–137, June 1993.
L. M. Chirica and D. F. Martin. Towards compiler implementation correctness proofs. ACM Transactions on Programming Languages and Systems, 8(2):185–214, April 1986.
J. W. de Bakker. Mathematical Theory of Program Correctness. Prentice-Hall, 1980.
E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.
E. W. Dijkstra and C. S. Scholten. Predicate Calculus and Program Semantics. Texts and Monographs in Computer Science. Springer-Verlag, 1990.
W. Goerigk, A. Dold, T. Gaul, G. Goos, A. Heberle, F. Henke, U. Hoffmann, H. Langmaack, H. Pfeifer, H. Ruess, and W. Zimmermann. Compiler correctness and implementation verification: The Verifix approach. In P. Fritzson, editor, Proc. Poster Session CC’96, pages 65–73, IDA Technical Report LiTH-IDA-R-96-12, Link∅ping, Sweden, 1996.
D. Gries. The Science of Programming. Springer-Verlag, 1981.
J. D. Guttman, J. D. Ramsdell, and M. Wand. VLISP: A verified implementation of Scheme. Lisp and Symbolic Computation, 8:5–32, 1995.
C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–583, 1969.
C. A. R. Hoare, H. Jifeng, and A. Sampaio. Normal form approach to compiler design. Acta Informatica, 30:701–739, 1993.
H. Langmaack. Software engineering for certification of systems: Specification, implementation, and compiler correctness (in German). Informationstechnik und Technische Informatik, 39(3):41–47, 1997.
J. S. Moore. Piton, A Mechanically Verified Assembly-Level Language. Kluwer Academic Publishers, 1996.
C. Morgan and T. Vickers, editors. On the Refinement Calculus. Springer-Verlag, 1994.
J. M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9:287–306, 1987.
P. D. Mosses. Action Semantics. Cambridge University Press, 1992.
S. S. Muchnick. Advanced compiler design implementation. Morgan Kaufmann Publishers, San Francisco, California, 1997.
M. Müller-Olm. Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction, LNCS 1283. Springer-Verlag, 1997.
T. S. Norvell. Machine code programs are predicates too. In D. Till, editor, 6th Refinement Workshop, Workshops in Computing. Springer-Verlag and British Computer Society, 1994.
E. Pofahl. Methods used for inspecting safety relevant software. In W. J. Cullyer, W. A. Halang, and B. J. Krämer, editors, High Integrity Programmable Electronics, pages 13–14. Dagstuhl-Sem.-Rep. 107, 1995.
S. Sippu and E. Soisalon-Soininen. Parsing Theory Vol. I. Springer-Verlag, 1988.
W. M. Waite and G. Goos. Compiler Construction. Springer-Verlag, 1984.
R. Wilhelm and D. Maurer. Übersetzerbau. Springer, 1992.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Müller-Olm, M., Wolf, A. (1999). On excusable and inexcusable failures towards an adequate notion of translation correctness. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_9
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive