Functional Dependencies and Moore-Set Completions of Abstract Interpretations and Semantics
Roberto Giacobazzi, Francesco Ranzato · The MIT Press eBooks · 1995
We introduce the notion of functional dependencies of abstract interpretations rela-tively 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 autodepen-dencies, 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 depen-dencies can be applied in collecting semantics design by abstract interpretation to systematically derive compositional semantics for logic programs. 1