Abstract
We present a language and semantics-independent, compositional and inductive method for specifying formal semantics or semantic properties of programs in equivalent fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form. The definitional method is obtained by extending set-theoretic definitions in the context of partial orders. It is parameterized by the language syntax, by the semantic domains and by the semantic transformers corresponding to atomic and compound program components. The definitional method is shown to be preserved by abstract interpretation in either fixpoint, equational, constraint, closure-condition, rule-based or game-theoretic form. The features common to all possible instantiations are factored out thus allowing for results of general scope such as well-definedness, semantic equivalence, soundness and relative completeness of abstract interpretations, etc. to be proved compositionally in a general language and semantics-independent framework.
This work was partly supported by Esprit BRA 8130 LOMAPS.
Chapter PDF
References
S. Abramsky, R. Jagadeesan, & P. Malacaria. Full abstraction for PCF (extended abstract). Proc. TACS'94, LNCS 789, 1–15, 1994.
P. Aczel. An introduction to inductive definitions. In J. Barwise, ed., Handbook of Mathematical Logic, vol. 90, 739–782. Elsevier, 1977.
J. Berstel & L. Boasson. Context-free languages. In [18], ch. 2, 61–102.
P. Cousot. Methods and logics for proving programs. In [18], ch. 15, 843–993.
P. Cousot et R. Cousot. Static determination of dynamic properties of recursive procedures. In E. Neuhold, ed., IFIP Conference on Formal Description of Programming Concepts, St-Andrews, N.B., Canada, 237–277. North-Holland Pub. Co., 1977.
P. Cousot & R. Cousot. Systematic design of program analysis frameworks. In 6 th ACM POPL, 269–282, 1979.
P. Cousot & R. Cousot. A language independent proof of the soundness and completeness of generalized Hoare logic. Inf. & Comp., 80(2):165–191, 1989.
P. Cousot & R. Cousot. Inductive definitions, semantics and abstract interpretation. In 196 th ACM POPL, 83–94, 1992.
P. Cousot & R. Cousot. Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages). In Proc. IEEE 1994 ICCL, 95–112, 1994.
L. Damas & R. Milner. Principle type schemes for functional programs. In 96 th ACM POPL, 207–212, 1982.
N. Heintze. Set-based analysis of ML programs (extended abstract). In Proc. ACM Conf. Lisp & Func. Prog., 1994.
C. A. R. Hoare. An axiomatic basis for computer programming. Comm. ACM, 12(10):576–580, 583, 1969.
R. Milner. A complete axiomatization for observational congruence of finite state behaviors. Inf. & Comp., 81:227–247, 1989.
P. D. Mosses. Denotational semantics. In [18], ch. 11, 575–631.
J. Palsberg & P. O'Keefe. A type system equivalent to flow analysis. In 226 th ACM POPL, 367–378, 1995.
J. Palsberg & M. I. Schwartzbach. Binding-time analysis: Abstract interpretation versus type inference. In Proc. IEEE 1994 ICCL, 289–298, 1994.
G. D. Plotkin. A structural approach to operational semantics. Tech. Rep. DAIMI FN-19, Aarhus University, (DK), Sept. 1981.
J. van Leeuwen, ed. Formal Models and Semantics, vol. B of Handbook of Theoretical Computer Science. Elsevier, 1990.
M. Wirsing. Algebraic specifications. In [18], ch. 13, 675–788.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cousot, P., Cousot, R. (1995). Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form. In: Wolper, P. (eds) Computer Aided Verification. CAV 1995. Lecture Notes in Computer Science, vol 939. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60045-0_58
Download citation
DOI: https://doi.org/10.1007/3-540-60045-0_58
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60045-9
Online ISBN: 978-3-540-49413-3
eBook Packages: Springer Book Archive