"Rule-Based Specifications and their Abstract Interpretation"
Compositional fixpoint presentations of semantics have been used for a long time in traditional denotational semantics as well as program static analysis by abstract interpretation [1]. In the last decade, the emergence of structured operational semantics has moved the preferred presentation style of semantics to rule-based formal systems and the same style of presentation has been used e.g. for typing and more generally program analysis [3].
Such compositional and inductive set-theoretic rule-based definitional methods can be extended in the context of partial orders for specifying formal semantics or semantic properties of programs in equivalent fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form. These various specification styles are preserved by abstract interpretation [3].
In this lecture we present non-classical rule-based semantics specifications and corresponding proof methods thus allowing for natural bi-inductive reasonings combining induction and co-induction. This is applied to denotational semantics, generalized weakest predicate transformers and comportment analysis.
[1] P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Conf. Rec. 6th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, pages 269-282, San Antonio, Texas, 1979.
[2] P. Cousot and R. Cousot. Inductive definitions, semantics and abstract interpretation. In Conf. Record of the 19th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, pages 83-94, Alburquerque, New Mexico, 1992.
[3] P. Cousot and R. Cousot. Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form, invited paper. In P. Wolper, editor. Proc. 7th Int. Conf. on Computer Aided Verification, CAV'95, Liege, Belgium, LNCS 939, pages 293-308, Springer-Verlag, 3-5 July 1995.