Tech Report CS-92-12
Reexecution in Abstract Interpretation of Prolog
Baudouin Le Charlier and Pascal Van Hentenryck
Logic programming, because of referential transparency, enjoys the property that a goal may be reexecuted arbitrarily often without affecting the meaning of the program. This property, although not interesting computationally in general, can be exploited in abstract interpretation to improve the accuracy of the analysis, as noted by Bruynooghe.
In this paper, we study reexecution from its theoretical foundations to its experimental evaluation. We define a new abstract semantics for Prolog that incorporates the notion of reexecution, and we study its correctness and precision properties. A fixpoint algorithm to compute (parts of) the abstract semantics is then presented. The accuracy and efficiency of the algorithm is evaluated experimentally on two abstract domains, a simple domain and an elaborate domain, and compared with conventional approaches.
The experimental results indicate that (1) reexecution can provide significant gain in accuracy at a very reasonable computation cost and that (2) reexecution on a simple domain is a versatile alternative to the standard approach on a more sophisticated domain.
(complete text in pdf)