Compositionality in the puzzle of semantics
Roberto Giacobazzi, Isabella Mastroeni · 2002
In this paper we study the connection between the structure of relational abstract domains for program analysis and compositionality of the underlying semantics. Both can be systematically designed as solution of the same abstract domain equation involving the same domain refinement: the reduced power operation. We prove that most well-known compositional semantics of imperative programs, such as the standard denotational and weakest precondition semantics can be systematically derived as solutions of simple abstract domain equations. This provides an equational presentation of both semantics and abstract domains for program analysis in a unique formal setting. Moreover both finite and transfinite compositional semantics share the same structure, and this allows us to provide consistent models for program manipulation. Categories and Subject Descriptors D.3 [Programming languages]: Formal definitions and theory---Semantics; F.3 [Logics and meanings of programs ]: Semantics of Programming Languages---algebraic approaches to semantics, denotational semantics, operational semantics General Terms Theory, Verification Keywords Abstract interpretation, reduced power, compositional semantics, transfinite semantics, program manipulation. 1.