Proving the correctness of storage representations

ABSTRACT

Conventional techniques for semantics-directed compiler derivation yield abstract machines that manipulate trees. However, in order to produce a real compiler, one has to represent these trees in memory. In this paper we show how the technique of storage-layout relations can be applied to verify the correctness of storage representations in a very general way. This technique allows us to separate denotational from operational reasoning, so that each can be used when needed. As an example, we show the correctness of a stack implementation of a language including dynamic catch and throw. The representation uses static and dynamic links to thread the environment and continuation through the stack. We discuss other uses of these techniques.

REFERENCES

• 1: Appel, A.W., "Runtime Tags Alen't Necessary," Lisp and Symbolt. c Com, putcttzotz 2 (1989), 153-162.
• 2: Dominique Clément , Thierry Despeyroux , Gilles Kahn , Joëlle Despeyroux, A simple applicative language: mini-ML, Proceedings of the 1986 ACM conference on LISP and functional programming, p.13-27, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319847]
• 3: William Clinger, The scheme 311 compiler an exercise in denotational semantics, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.356-364, August 06-08, 1984, Austin, Texas, United States [doi>10.1145/800055.802052]
• 4: J Rees , W Clinger, Revised report on the algorithmic language scheme, ACM SIGPLAN Notices, v.21 n.12, p.37-79, Dec. 1986 [doi>10.1145/15042.15043]
• 5: Daniel P. Friedman , Christopher T. Haynes , Mitchell Wand, Essentials of programming languages, MIT Press, Cambridge, MA, 1992
• 6: Benjamin Goldberg, Tag-free garbage collection for strongly typed programming languages, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.165-176, June 24-28, 1991, Toronto, Ontario, Canada
• 7: John Hannan, Making abstract machines less abstract, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.618-635, June 1991, Cambridge, Massachusetts, United States
• 8: Peter Lee, Topics in advanced language implementation, MIT Press, Cambridge, MA, 1991
• 9: Farmer, W.M, Guttman, J.D., Monk, L.G., Ramsdell, J D., and Swarup. V. "VLISP. A Verified Language Implementation FY 91 Year-End Report," The MITRE Corporation Technical Report MTR11232, October, 1991.
• 10: Oliva, D.P., and Wand, M., "A Verified Compiler for Pure PreScheme," Final Report fox MITRE Contract Number F19628-89-C-001. Included in {9}.
• 11: McCarthy, J. and Painter, J. "Correctness of a Compiler for Arithmetic Expressions," in Proc. Symp. in Appl. Math., Vol. 19, Mathematical Aspects of Computer Science (J. T. Schwartz, ed.) Amer. Math. Soc., Providence, RI, 1967, 33-41.
• 12: Robert Milne , C. Strachey, A Theory of Programming Language Semantics, Halsted Press, New York, NY, 1977
• 13: Plotkin, G.D. "Call-by-Name, Call-by-Value and the X- Calculus," Theoret. Comp Sci 1 (1975) 125-159.
• 14: Jean-Claude Raoult , Ravi Sethi, The global storage needs of a subcomputation, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.148-157, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800526]
• 15: John C. Reynolds, The Craft of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1981
• 16: David A. Schmidt, Denotational semantics: a methodology for language development, William C. Brown Publishers, Dubuque, IA, 1986
• 17: Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA, 1977
• 18: Mitchell Wand, Semantics-directed machine architecture, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.234-241, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582179]
• 19: Mitchell Wand, Loops in combinator-based compilers, Information and Control, v.57 n.2-3, p.148-164, May/June 1983 [doi>10.1016/S0019-9958(83)80041-2]
• 20: Mitchell Wand, Correctness of Procedure Representations in Higher-Order Assembly Language, Proceedings of the 7th International Conference on Mathematical Foundations of Programming Semantics, p.294-311, March 25-28, 1991

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

  E. Data
  E.1 DATA STRUCTURES
      Subjects: Trees

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Languages, Verification