Computing Reviews

Improving abstract interpretations by combining domains
Codish M., Mulkers A., Bruynooghe M., de la Banda M., Hermenegildo M. ACM Transactions on Programming Languages and Systems17(1):28-44,1995.Type:Article
Date Reviewed: 09/01/96

In the abstract setting of domain theory, the meaning of a program P is expressed as the least fixed point of a monotonic operator f P on a domain E. In the development of the program, one leaves out the special features of the concrete data. This process can be seen as the definition of a new domain D linked to E by two monotonic operators, abstraction α : E → D and concretization &ggr; : D → E, for which α ( &ggr; ( d ) ) = d and e ≤ &ggr; ( α ( e ) ) (≤ being the natural order on E). Next, one must approximate f P by an operator g : D → D, which has a finitely computable least fixed point.

D is not unique, however; intuitively, such a D gives greater emphasis to a particular type of information available from the concrete data. So it is natural to search for a way to merge two or more abstraction domains.

There is a direct product construct, but it corresponds to performing only independent analyses of each of the factors. The aim of this paper is to describe a new operation, the reduced product, which removes redundant information between the factors and thus increases efficiency. The authors give constructive definitions of reduced products for examples dealing with the sharing of variables in logic programs, and compare them with other recent analyses.

The theory of logic programming has a reputation for being cryptic, a reputation from which this paper does not depart: written in a compact style, especially for the examples, it is hard to read, even for a research paper.

Reviewer:  F. Aribaud Review #: CR119221 (9609-0716)

Reproduction in whole or in part without permission is prohibited.   Copyright 2024 ComputingReviews.com™
Terms of Use
| Privacy Policy