A Characterization of Symmetric Semantics by Domain Complementation

Roberto Giacobazzi and Isabella Mastroeni

To appear at the 2nd International Conference on Principles and Practice of Declarative Programming (PPDP 2000), Montreal, Canada, September 20-22, 2000


In this paper 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 derive 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 demoniac/infinite 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 of cc as abstract interpretation of maximal traces of constraints.