Operators that systematically produce more precise abstract interpretations from simpler ones are interesting. In this paper we present a formal study of one such operator: the powerset. The main achievements of the paper are described below: (1) A formal definition of the powerset operator is given. For any given abstract interpretation bD=<D,o_1,…,o_k>, where D is the abstract domain and o_1,…,o_k are the abstract operations, this operator provides a new abstract interpretation P(bD)=<P(D),o_1^*,…,o_k^*>. Thus, the powerset concerns also the abstract operations o_i^*, that are constructively defined from the o_i's. (2) A necessary and sufficient condition guaranteeing that P(D) is strictly better than D is given. (3) The general theory is applied to the well-known abstract interpretation PROP for ground-dependence analysis of logic programs. It is shown that P(PROP) is strictly better than PROP.

Improving Abstract Interpretations by Systematic Lifting to the Powerset

RANZATO, FRANCESCO
1994

Abstract

Operators that systematically produce more precise abstract interpretations from simpler ones are interesting. In this paper we present a formal study of one such operator: the powerset. The main achievements of the paper are described below: (1) A formal definition of the powerset operator is given. For any given abstract interpretation bD=, where D is the abstract domain and o_1,…,o_k are the abstract operations, this operator provides a new abstract interpretation P(bD)=. Thus, the powerset concerns also the abstract operations o_i^*, that are constructively defined from the o_i's. (2) A necessary and sufficient condition guaranteeing that P(D) is strictly better than D is given. (3) The general theory is applied to the well-known abstract interpretation PROP for ground-dependence analysis of logic programs. It is shown that P(PROP) is strictly better than PROP.
1994
1994 Joint Conference on Declarative Programming, GULP-PRODE'94 Peñiscola, Spain
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

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/11577/2509502
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? 12
social impact