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
Abstract
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.