A characterization of symmetric semantics by domain complementation

By: Roberto Giacobazzi and Isabella Mastroeni

Roberto Giacobazzi
Dip. Scientifico e Tecnologico
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2
I-37134 Verona, Italy


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/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 as abstract interpretation of maximal traces of constraints.
Related papers:
  • Complementation in abstract interpretation (ACM TOPLAS 19(1):7-47, 1997)
  • A Unifying View on Abstract Domain Design (ACM Comp. Surveys 28(2), 1996)
  • Weak Relative Pseudo-Complements of Closure Operators (Alg. Univ. 36(3):405-412, 1996)
  • Complementing Logic Program Semantics (LNCS 1139, Springer-Verlag, 1996)
  • Functional Dependencies and Moore-Set Completions of Abstract Interpretations and Semantics (ILPS'95, The MIT Press, 1995)

  • Available: DVI, PostScript, BibTeX Entry.