Inductive definitions, semantics and abstract interpretations

ABSTRACT

We introduce and illustrate a specification method combining rule-based inductive definitions, well-founded induction principles, fixed-point theory and abstract interpretation for general use in computer science. Finite as well as infinite objects can be specified, at various levels of details related by abstraction. General proof principles are applicable to prove properties of the specified objects. The specification method is illustrated by introducing G ∞ SOS, a structured operational semantics generalizing Plotkin's [28] structured operational semantics (SOS) so as to describe the finite, as well as the infinite behaviors of programs in a uniform way and by constructively deriving inductive presentations of the other (relational, denotational, predicate transformers, …) semantics from G ∞ SOS by abstract interpretation.

REFERENCES

• 1: P. Aczel. An introduction to inductive definitions. In J. Barwise, ed., Handbook o} Mathematical Logic, Elsevier, 739-782, 1977.
• 2: Krzysztof R. Apt, Logic programming, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 3: K. R. Apt , G. D. Plotkin, Countable nondeterminism and random assignment, Journal of the ACM (JACM), v.33 n.4, p.724-767, Oct. 1986 [doi>10.1145/6490.6494]
• 4: E. Astesiano. Inductive semantics. In E.J. Neuhold & M. Paul, eds., Formal Description of Programming Concepts, Springer, 1990.
• 5: J. Barwise. Mixed fixed poims, in vol. 17 of CSLI lecture notes, 285-287, CSLI/Stanf0rd, 1989.
• 6: Roland Bol , Jan Friso Groote, The meaning of negative premises in transition system specifications (extended abstract), Proceedings of the 18th international colloquium on Automata, languages and programming, p.481-494, June 1991, Madrid, Spain
• 7: P. Cousot. Semantic foundations of program analysis. In S.S. Muchnick & N.D. Jones, ads., Program Flow Analysis: Theory and Applications, 303-342, Prentice-Hall, 1981.
• 8: 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]
• 9: P. Cousot & R. Cousot. Constructive versions of Tarski's fixed point theorems. Pacific J. of Math., 82(1):43-57, 1979.
• 10: 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]
• 11: P. Cousot & 1%. Cousot. Induction principles for proving invariance properties of programs, In E. Neel, ed., Tools and Notions for Program Construction, 43-I19, Cambridge U- niv. Press, 1982.
• 12: P Cousot , R Cousot, “A la Floyd” induction principles for proving inevitability, Algebraic methods in semantics, Cambridge University Press, New York, NY, 1986
• 13: P. Degano , R. De Nicola , U. Montanari, A partial ordering semantics for CCS, Theoretical Computer Science, v.75 n.3, p.223-262, Oct. 1990 [doi>10.1016/0304-3975(90)90095-Y]
• 14: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 15: S. Feferman. Formal theories for transfinite iterations of generalized inductive definitions and some subsystems of analysis, In A. Kino, J. Myhill & R.E. Vesley, eds., Intuitionism and Proof Theory, 303-326, North Holland, 1970.
• 16: Jan Friso Groote, Transition system specifications with negative premises (extended abstract), Proceedings on Theories of concurrency : unification and extension: unification and extension, p.332-341, September 1990, Amsterdam, The Netherlands
• 17: C. A. Gunter , D. S. Scott, Semantic domains, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 18: G. Kahn, Natural Semantics, Proceedings of the first Franco-Japanese Symposium on Programming of future generation computers, p.237-257, August 1988, Tokyo, Japan
• 19: K. Kunen. Declarative semantics of logic programming. Bull. EATCS 44:147-167, 1991.
• 20: J.-L. Lassez & M.J. Maher. Closure and fairness in the semantics of programming logic. TCS 29:167-184, 1984.
• 21: Robin Milner, Operational and algebraic semantics of concurrent processes, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 22: Robin Milner , Mads Tofte, Co-induction in relational semantics, Theoretical Computer Science, v.87 n.1, p.209-220, Sept. 16, 1991 [doi>10.1016/0304-3975(91)90033-X]
• 23: Peter D. Mosses, Denotational semantics, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 24: A. Mycroft. Abstract interpretatio~z and optimisin9 trans- 81, Univ. of Edinburgh, 1981.
• 25: F. Nielson. A denotational framework for data flow analysis. Acts informatica, 18:265-287, 1982.
• 26: David Park, On the Semantics of Fair Parallelism, Proceedings of the Abstract Software Specifications, 1979 Copenhagen Winter School, p.504-526, January 22-February 02, 1979
• 27: G.D. Plotkin. Call-by-name, call-by-value and the X- cMculus. TGS 1:125-159, 1975.
• 28: G.D. Plotkin. A structural approach to operational semantics. Tech. Rap. DAIMI FN-19, Aarhus Univ., 1981.
• 29: Gianna Reggio, A non-standard inductive semantics, Proceedings of the tenth conference on Foundations of software technology and theoretical computer science, p.362-372, November 1990, Bangalore, India
• 30: M. H. Van Emden , R. A. Kowalski, The Semantics of Predicate Logic as a Programming Language, Journal of the ACM (JACM), v.23 n.4, p.733-742, Oct. 1976 [doi>10.1145/321978.321991]
• 31: Jan van Leeuwen, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics

Additional 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

General Terms:
Algorithms