Detecting global variables in denotational specifications

ABSTRACT

Sufficient criteria are given for replacing all occurrences of the store argument in a Scott-Strachey denotational definition of a programming language by a single global variable. The criteria and transformation are useful for transforming denotational definitions into compilers and interpreters for imperative machines, for optimizing applicative programs, and for judging the suitability of semantic notations for describing imperative languages. An example transformation of a semantics of a repeat-loop language to one which uses a global store variable is given to illustrate the technique.

REFERENCES

• 1: BJ~RNER, D. Rigorous development of interpreters and compilers. In D. Bj~rner and C. Jones (Eds.), Formal Specification and Software Development. Prentice-Hall, Englewood Cliffs, N.J., 1982, pp. 271-320.
• 2: CURRY, H. B., AND FEYS, R. Cornbinatory Logic, Vol. 1. Elsevier North-Holland, New York, 1958.
• 3: Joseph A. Goguen , Kamran Parsaye-Ghomi, Algebraic Denotational Semantics Using Parameterized Abstract Modules, Proceedings of the International Colloquium on Formalization of Programming Concepts, p.292-309, April 19-25, 1981
• 4: HOARE, C. A.R. Proof of correctness of data representations. Acta Inf. I (1972), 271-281.
• 5: HUET, G., AND OPPEN, D. Equations and rewrite rules: A survey. In R. Book (Ed.), Formal Language Theory: Perspectives and Open Problems. Academic Press, New York, 1980, pp. 349- 405.
• 6: JONES, C.B. The meta language. In D. Bjzrner and C. Jones (Eds.), Formal Specification and Software Development. Prentice-Hall, Englewood Cliffs, N.J., 1982, pp. 271-320.
• 7: Neil D. Jones, Semantics-Directed Compiler Generation: Proceedings, Springer-Verlag New York, Inc., Secaucus, NJ, 1980
• 8: JONES, N. D., MUCHNICK, S. S., AND SCHMWT, D.A. A universal compiler. Tech. Rep. DAIMI IR-17, Computer Science Dept., Univ. Aarhus, Denmark, 1979.
• 9: MOSSES, P.D. Making denotational semantics less concrete. Presented at the workshop on semantics of programming languages, Bad Honnef, Germany, 1977.
• 10: MOSSES, P.D. SIS--Reference manual and user's guide. Tech. Rep. DAIMI MD-30, Computer Science Dep., Univ. Aarhus, Denmark, 1979.
• 11: Peter D. Mosses, A constructive approach to compiler correctness, Semantics-Directed Compiler Generation, Proceedings of a Workshop, p.189-210, January 14-18, 1980
• 12: Peter D. Mosses, A Semantic Algebra for Binding Constructs, Proceedings of the International Colloquium on Formalization of Programming Concepts, p.408-418, April 19-25, 1981
• 13: MOSSES, P.D. Abstract semantic algebras! In Formal Description of Programming Concepts II. Elsevier North-Holland, New York, 1983.
• 14: MYCROFT, A. Abstract interpretation and optimizing transformations for applicative programs. Ph.D. Dissertation, Computer Science Dep., Univ. Edinburgh, Scotland, 1981.
• 15: Michael J. O'Donnell, Computing in Systems Described by Equations, Springer-Verlag New York, Inc., Secaucus, NJ, 1977
• 16: PLOTKIN, G. LCF considered as a programming language. Theor. Comput. Sci. 5(1977), 223- 255.
• 17: PLOTKIN, G. The category of complete partial orders. In Proceedings, Summer School on Foundations of Artificial Intelligence and Computer Science (Institute di Scienze dell' Informazione, Universita di Pisa), 1978.
• 18: Jean-Claude Raoult , Ravi Sethi, Properties of a Notation for Combining Functions, Proceedings of the 9th Colloquium on Automata, Languages and Programming, p.429-441, July 12-16, 1982
• 19: 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]
• 20: John C. Reynolds, Definitional interpreters for higher-order programming languages, Proceedings of the ACM annual conference, p.717-740, August 01-01, 1972, Boston, Massachusetts, United States [doi>10.1145/800194.805852]
• 21: SCHMIDT, D.A. Denotational semantics as a programming language. Internal Rep. CSR-100, Computer Science Dep., Univ. Edinburgh, Scotland, 1982.
• 22: SCHMIOT, D. A. Detecting global variables in denotational specifications (extended version). Tech. Rep. 84-3, Computer Science Dep., Iowa State Univ., Ames, Iowa, 1984.
• 23: STOY, J. Denotational Semantics. MIT Press, Cambridge, Mass., 1977.
• 24: WAND, M. First order identities as a defining language. Acta Inf. 14(1980), 337-357.
• 25: 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]
• 26: Mitchell Wand, Deriving Target Code as a Representation of Continuation Semantics, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.496-517, July 1982 [doi>10.1145/357172.357179]
• 27: WEONER, P. Programming language semantics. In R. Rustin (Ed.), Formal Semantics of Programming Languages. Prentice-Hall, Englewood Cliffs, N.J., 1972, pp. 149-248.

INDEX TERMS

Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Denotational semantics
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Languages, Theory, Verification