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=. 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.
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.