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.

Functional Dependencies and Moore-Set Completions of Abstract Interpretations and Semantics

GIACOBAZZI, Roberto;
1995

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.
0262620995
Abstract interpretation; logic programs; lattice theory
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/438340
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact