Program transformations in a denotational setting

ABSTRACT

Program transformations are frequently performed by optimizing compilers, and the correctness of applying them usually depends on data flow information. For language-to-same-language transformations, it is shown how a denotational setting can be useful for validating such program transformations. Strong equivalence is obtained for transformations that exploit information from a class of forward data flow analyses, whereas only weak equivalence is obtained for transformations that exploit information from a class of backward data flow analyses. To obtain strong equivalence, both the original and the transformed program must be data flow analysed, but consideration of a transformation-exploiting liveness of variables indicates that a more satisfactory approach may be possible.

REFERENCES

• 1: Alfred V. Aho , Jeffrey D. Ullman, Principles of Compiler Design (Addison-Wesley series in computer science and information processing), Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1977
• 2: Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
• 3: COUSOT, P. Semantic foundations of program analysis. In Program Flow Analysis: Theory and Applications, S. S. Muchnick and N. D. Jones, Eds., Prentice-Hall, Englewood Cliffs, N.J., 1981, 303-342.
• 4: Susan L. Gerhart, Correctness-preserving program transformations, Proceedings of the 2nd ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.54-66, January 20-22, 1975, Palo Alto, California [doi>10.1145/512976.512983]
• 5: HUET, G., ANO LANG, B. Proving and applying program transformations expressed with secondorder patterns. Acta In{. 11 (1978), 31-55.
• 6: David B. Loveman, Program Improvement by Source-to-Source Transformation, Journal of the ACM (JACM), v.24 n.1, p.121-145, Jan. 1977 [doi>10.1145/321992.322000]
• 7: Robert Milne , C. Strachey, A Theory of Programming Language Semantics, Halsted Press, New York, NY, 1977
• 8: MILNER, R. Program semantics and mechanized proof. In Foundations of Computer Science II, K. R. Apt and J. W. de Bakker, Eds., Mathematical Centre Tracts 82, Amsterdam, 1976, 3-44.
• 9: NIELSON, F. A denotational framework for data flow analysis. Acta Inf. 18 (1982), 265-287.
• 10: Barry K. Rosen, Tree-Manipulating Systems and Church-Rosser Theorems, Journal of the ACM (JACM), v.20 n.1, p.160-187, Jan. 1973 [doi>10.1145/321738.321750]
• 11: Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA, 1977

INDEX TERMS

Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics
      D.3.4 Processors
          Subjects: Optimization; Compilers

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification
      F.3.2 Semantics of Programming Languages
          Subjects: Denotational semantics

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming
          Subjects: Program transformation

General Terms:
Design, Languages, Theory, Verification