Functional Dependencies and Moore-Set Completions of Abstract Interpretations and Semantics
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:
We introduce the notion of functional dependencies of abstract interpretations
relatively to a binary operator of composition.
Functional dependencies are obtained by a functional composition
of abstract domains, and provide a systematic approach to
construct new abstract domains.
In particular, we study the case of autodependencies,
namely monotone operators on a given abstract domain. Under suitable
hypotheses, this corresponds to a Moore-set completion
of the abstract domain, providing a compact lattice-theoretic
representation for dependencies.
We prove that
the abstract domain Def
for ground-dependency analysis of logic programs can
be systematically derived by autodependencies of a more abstract
(and simple) domain for pure groundness analysis.
Furthermore, we show that functional
dependencies can be applied in collecting semantics design
by abstract interpretation to systematically
derive compositional semantics for logic programs.
Available:
DVI,
PostScript,
BibTeX Entry.
giaco@di.unipi.it