3.2 Abstract Interpretation for (Constraint) Logic
M. Bruynooghe and D. Boulanger
Katholieke Universiteit Leuven
Celestijnenlaan 200, AB 3001 Heverlee, Belgium
The theory of abstract interpretation, initially developed by the Cousot's for imperative languages has been adapted to logic programming where it has become a very active area of research, illustrated by the list of references in the survey paper (CoC92b). It has reached a level of maturity where it is included as an optimisation tool in some prototype implementations of Prolog. In recent years, also abstract interpretation of constraint logic programming has been studied. Abstract interpretation is an area where the majority of publications is very technical in nature. This tutorial aims at making the topic more accessible to newcomers. Therefore, we have tried to present the main intuitions in a rather informal way. We have preferred informal accounts above very precise but rigid and hard to penetrate formalism. The paper is not a survey, so although we give some entry points to the literature, we have not aimed at completeness.
A flrst part discusses the framework of abstract interpretation in very general terms, as a way to approximate the semantics which has to be formulated as a flxpoint of some function. A second part applies this theory to logic programming, at the same time showing general examples of the theory, and explaining some of the major approaches towards abstract interpretation of logic programs. A third and a flnal part tries to explain that the step from logic programming to constraint logic programming is a small one and that frameworks developed for abstract interpretation of logic programs carry over to constraint logic programming.
This chapter assumes some familiarity with the basic notions of logic programming and with the concept of flxpoint. The reader can flnd material concerning these in (Llo87).
3.2.1 Basic Principles
22.214.171.124 Abstracting computations As part of our education we have learned to compute properties of the results of calculations by performing approximate or abstract computations. The general idea is to abstract the operands, apply an abstract operator and to obtain a result which is the abstraction of the result of the concrete operation.
A typical example mastered in the flrst years of school, is the multiplication of multidigit numbers. To check against silly errors, due to a slip of our mind,