The reduced relative power operation on abstract domains
By: R. Giacobazzi and F. Ranzato
Roberto
Giacobazzi
Dip. di Informatica
Univ. di Pisa
Corso
Italia 40, 56125 Pisa
(Italy)
giaco@di.unipi.it
Abstract:
In the context of standard abstract interpretation theory, we define
and study a systematic operator of reduced relative power for
composing functionally abstract domains. The reduced relative power of
two abstract domains D1 (the exponent) and D2 (the
base) consists in a suitably defined lattice of monotone functions
from D1 to D2, called dependencies, and it is a
generalization of the Cousot and Cousot operator of reduced (cardinal)
power. The relationship between the reduced relative power and
Nielson's tensor product is also investigated. The case of
autodependencies (when base and exponent are the same domain) turns
out to be particularly interesting: Under certain hypotheses, the
domain of autodependencies corresponds to a suitable powerset-like
completion of the base abstract domain, providing a compact
set-theoretic representation for autodependencies. The usefulness of
the reduced relative power is shown by a number of applications to
abstract domains used both for program analysis and for semantics
design. Notably, we prove that the domain Def for logic
program ground-dependency analysis can be characterized as
autodependencies of a standard more abstract domain representing plain
groundness only, and we show how to exploit reduced relative power to
systematically derive compositional logic program semantics. This
paper is an extended version of
Functional dependencies and Moore-set completions of abstract
interpretations and semantics (ILPS'95, 1995).
Available: DVI,
PostScript,
BibTeX Entry.
Related works by the authors:
giaco@sci.univr.it