TY - GEN
T1 - Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form
AU - Cousot, Patrick
AU - Cousot, Radhia
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1995.
PY - 1995
Y1 - 1995
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84947934484&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84947934484&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:84947934484
SN - 9783540600459
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 293
EP - 308
BT - Computer Aided Verification - 7th International Conference, CAV 1995, Proceedings
A2 - Wolper, Pierre
PB - Springer Verlag
T2 - 7th International Conference on Computer Aided Verification, CAV 1995
Y2 - 3 July 1995 through 5 July 1995
ER -