Natural semantics as a static program analysis framework

ABSTRACT

Natural semantics specifications have become mainstream in the formal specification of programming language semantics during the last 10 years. In this article, we set up sorted natural semantics as a specification framework which is able to express static semantic information of programming languages declaratively in a uniform way and allows one at the same time to generate corresponding analyses. Such static semantic information comprises context-sensitive properties which are checked in the semantic analysis phase of compilers as well as further static program analyses such as, for example, classical data and control flow analyses or type and effect systems. The latter require fixed-point analyses to determine their solutions. We show that, given a sorted natural semantics specification, we can generate the corresponding analysis. Therefore, we classify the solution of such an analysis by the notion of a proof tree. We show that a proof tree can be computed by solving an equivalent residuation problem. In case of the semantic analysis, this solution can be found by a basic algorithm. We show that its efficiency can be enhanced using solution strategies. We also demonstrate our prototype implementation of the basic algorithm which proves its applicability in practical situations. With the results of this article, we have established natural semantics as a framework which closes the gap between declarative and operational specification methods for static semantic properties as well as between specification frameworks for the semantic analysis. In particular, we show that natural semantics is expressive enough to define fixed-point program analyses.

REFERENCES

• 1: Martin Abadi , Luca Cardelli, A Theory of Objects, Springer-Verlag New York, Inc., Secaucus, NJ, 1996
• 2: Andréka, H. and Németi, I. 1978. The generalized completeness of Horn predicate logic as a programming language. Acta Cybernet., 4, 3--10.
• 3: Attali, I. 1989. Compilation de programmes Typol par attributs sémantiques. Ph.D. dissertation, University of Nice, Nice, France.
• 4: Isabelle Attali , Denis Caromel , Sidi Ould Ehmety, A natural semantics for Eiffel dynamic binding, ACM Transactions on Programming Languages and Systems (TOPLAS), v.18 n.6, p.711-729, Nov. 1996 [doi>10.1145/236114.236118]
• 5: Attali, I. and Franchi-Zannettacci, P. 1988. Unification-free execution of Typol programs by semantic attribute evaluation. In International Conference Symposium on Logic Programming, (Seattle, Aug.). MIT Press, Cambridge, MA, 160--177.
• 6: Franz Baader, Unification Theory, Proceedings of the First International Workshop on Word Equations and Related Topics, p.151-170, October 01-03, 1990
• 7: Rolf Bahlke , Gregor Snelting, The PSG system: from formal language definitions to interactive programming environments, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.4, p.547-576, Oct. 1986 [doi>10.1145/6465.20890]
• 8: Gregor V. Bochmann, Semantic evaluation from left to right, Communications of the ACM, v.19 n.2, p.55-62, Feb. 1976 [doi>10.1145/359997.359999]
• 9: Giuseppe Castagna, Object-oriented programming: a unified foundation, Birkhauser Boston Inc., Cambridge, MA, 1997
• 10: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 11: Despeyroux, T. 1984. Executable specification of static semantics. In Semantics of Data Types, G. Kahn, Ed. Lecture Notes in Computer Science, vol. 173, Springer-Verlag, Berlin, Germany, 215--233.
• 12: Eric Domenjoud, A technical note on AC-unification. The number of minimal unifiers of the equation ax1+&cdots;+axp=&d2; ACby1+&cdots;+by q , Journal of Automated Reasoning, v.8 n.1, p.39-44, Feb. 1992
• 13: Sophia Drossopoulou , Susan Eisenbach, Describing the Semantics of Java and Proving Type Soundness, Formal Syntax and Semantics of Java, p.41-82, January 1999
• 14: Eli. n.d. Eli: Übersetzerentwicklung leicht gemacht. Available online at http://www.uni-paderborn.de/fachbereich/AG/agkastens/eli_home.html.
• 15: Geiβ, R. 1998. The Sherlock-System---a prototype for many-sorted natural semantics. Term project, Universität Karlsruhe, Fakultät für Informatik, Karlsruhe, Germany.
• 16: Geiβ, R. 1999. The Sherlock-System II---a prototype for many-sorted natural semantics implemented in Java. Term project. Universität Karlsruhe, Fakultät für Informatik, Karlsruhe, Germany.
• 17: Gentzen, G. 1935. Untersuchungen über das logische Schlieβen. Mathem. Zeitschrift 39, 176--210 and 405--431.
• 18: Glesner, S. 1998. Many-sorted natural semantics---specification and generation of the semantic analysis for imperative and object-oriented programming languages. Working paper 63. Westfälische Wilhelms-Universität Münster, Institut für Wirtschaftsinformatik, Münster, Germany. (Proceedings Workshop on Functional and Logic Programming).
• 19: Glesner, S. 1999a. Natural semantics for imperative and object-oriented programming languages. In Informatik '99---Informatik überwindet Grenzen, Proceedings der 29. Jahrestagung der Gesellschaft für Informatik (Paderborn, Oct.), K. Beiersdörfer, G. Engels, and W. Schäfer, Eds. GI-Gesellschaft für Informatik e.V., Springer-Verlag, Berlin, Germany 370--379.
• 20: Glesner, S. 1999b. Natürliche Semantik für imperative und objektorientierte Programmiersprachen. Ph.D. dissertation. Universität Karlsruhe, Fakultät für Informatik. Shaker Verlag, Aachen, Germany.
• 21: Glesner, S. and Zimmermann, W. 1997. Using many-sorted inference rules to generate semantic analysis. In Proceedings des Workshops der Informatik-Graduiertenkollegs "Promotion tut not: Innovationsmotor Graduiertenkolleg" im Rahmen der GI-Jahrestagung 1997, Otto Spaniol, Ed. Verlag der Augustinus Buchhandlung (Aachener Beiträge zur Informatik, Band 21), Aachen, Germany.
• 22: S. Glesner , W. Zimmermann, Using many-sorted natural semantics to specify and generate semantic analysis, Proceedings of the IFIP TC2 WG2.4 working conference on Systems implementation 2000 : languages, methods and tools: languages, methods and tools, p.249-262, January 1998, Berlin, Germany
• 23: J. Grosch , H. Emmelmann, A tool box for compiler construction, Proceedings of the third international workshop on Compiler compilers, p.106-116, February 1991, Schwerin, Germany
• 24: Hanus, M. 1994. The integration of functions into logic programming: From theory to practice. J. Logic Program. 19, 20, 583--628.
• 25: Atshushi Igarashi , Benjamin Pierce , Philip Wadler, Featherwieght Java: a minimal core calculus for Java and GJ, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.132-146, November 01-05, 1999, Denver, Colorado, United States
• 26: Pierre Jouvelot , David Gifford, Algebraic reconstruction of types and effects, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.303-310, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99623]
• 27: G. Kahn, Natural semantics, 4th Annual Symposium on Theoretical Aspects of Computer Sciences on STACS 87, p.22-39, February 1987, Passau, Germany
• 28: Deepak Kapur , Paliath Narendran, Complexity of unification problems with associative-commutative operators, Journal of Automated Reasoning, v.9 n.2, p.261-288, Oct. 1992 [doi>10.1007/BF00245463]
• 29: Kastens, U. 1980. Ordered attribute grammars. Acta Inform. 13, 3, 229--256.
• 30: Kastens, U. Hutt, B., and Zimmermann, E. 1982. GAG: A Practical Compiler Generator. Lecture Notes in Computer Science, vol. 141. Springer-Verlag, Heidelberg, Germany.
• 31: Knuth, D. E. 1968. Semantics of context-free languages. Math. Syst. Theor. 2, 2, 127--146.
• 32: Knuth, D. E. 1971. Semantics of context-free languages: Correction. Math. Syst. Theor. 5, 95--96.
• 33: A. J. Kfoury , J. Tiuryn , P. Urzyczyn, An analysis of ML typability, Journal of the ACM (JACM), v.41 n.2, p.368-398, March 1994 [doi>10.1145/174652.174659]
• 34: Lewis, P. M., Rosenkrantz, D. J., and Stearns, R. E. 1974. Attributed translations. J. Comput. Syst. Sci., 9, 3, 279--307.
• 35: Robin Milner , Mads Tofte, Commentary on standard ML, MIT Press, Cambridge, MA, 1991
• 36: Robin Milner , Mads Tofte , Robert Harper, The Definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 37: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• 38: Robert Morgan, Building an optimizing compiler, Digital Press, Newton, MA, 1998
• 39: Steven S. Muchnick, Advanced compiler design and implementation, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1998
• 40: Flemming Nielson , Hanne R. Nielson , Chris Hankin, Principles of Program Analysis, Springer-Verlag New York, Inc., Secaucus, NJ, 1999
• 41: Tobias Nipkow , David von Oheimb, Java_light is type-safe—definitely, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.161-170, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268960]
• 42: Martin Odersky, Defining context-dependent syntax without using contexts, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.3, p.535-562, July 1993 [doi>10.1145/169683.174159]
• 43: Oz. n.d. The Oz programming system. Programming Systems Lab, DFKI, and Universität des Saarlandes, Saarbrücken, Germany. Available online at http://www.ps.uni-sb.de/oz/.
• 44: Jens Palsberg , Michael I. Schwartzbach, Object-oriented type systems, John Wiley and Sons Ltd., Chichester, UK, 1994
• 45: Paterson, M. S. and Wegman, M. N. 1978. Linear unification. J. Comp. Syst. Sci. 16, 2, 158--167.
• 46: Pettersson, M. 1995. Compiling natural semantics. Ph.D. dissertation. Department of Computer and Information Science, Linköping University, Linköping, Sweden.
• 47: Mikael Pettersson, A Compiler for Natural Semantics, Proceedings of the 6th International Conference on Compiler Construction, p.177-191, April 24-26, 1996
• 48: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• 49: Gregor Snelting , Wolfgang Henhapl, Unification in many-sorted algebras as a device for incremental semantic analysis, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.229-235, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512665]
• 50: Don Syme, Proving Java Type Soundness, Formal Syntax and Semantics of Java, p.83-118, January 1999
• 51: von Oheimb, D. 2001. Analyzing Java in Isabelle/HOL. Ph.D. dissertation. Technische Universität München, Munich, Germany.
• 52: David von Oheimb , Tobias Nipkow, Machine-Checking the Java Specification: Proving Type-Safety, Formal Syntax and Semantics of Java, p.119-156, January 1999
• 53: Martin Wirsing, Algebraic specification, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991

INDEX TERMS

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

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics
      D.3.3 Language Constructs and Features
          Subjects: Constraints
      D.3.4 Processors
          Subjects: Translator writing systems and compiler generators

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.8 Problem Solving, Control Methods, and Search
          Subjects: Graph and tree search strategies

General Terms:
Languages

Keywords:
Natural semantics, compiler generators, constraint solving, fixed-point program analyses, semantic analysis, static program analysis