A characterization of symmetric semantics by domain complementation
Roberto Giacobazzi, Isabella Mastroeni · 2000
We characterize the symmetric structure of Cousot's hierarchy of semantics in terms of a purely algebraic manipulation of abstract domains. We consider domain complementation in abstract interpretation as a formal method for systematically deriving complementary semantics of programming languages. We prove that under suitable hypothesis the semantics abstraction commutes with respect to domain complementation. This result allows us to prove that angelic and demonic/innite semantics are complementary and provide a minimal decomposition of all natural-style trace-based, relational, denotational, Dijkstra's predicate transformer and Hoare's axiomatic semantics. We apply this construction to the case of concurrent constraint programming, characterizing well known semantics as abstract interpretation of maximal traces of constraints. Categories and Subject Descriptors D.3 [Programming languages]: Formal denitions and theory|Semantics; F.3 [Logics and meanings of programs ]: Semantics of...