REEXECUTION IN ABSTRACT INTERPRETATION OF PROLOG

Logic programming, because of referential transparency, enjoys the property that a literal may be reexecuted finitely 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 [6]. We study reexecution from its theoretical foundations to its experimental evaluation. We define a new abstract semantics for Prolog, which incorporates the notion of reexecution, and we study its correctness and precision properties. A fixpoint algorithm to compute the abstract semantics is then presented. The accuracy and efficiency of the algorithm is evaluated experimentally on two abstract domains, a simple and an elaborate one, and compared with conventional approaches. The experimental results indicate that (1) reexecution can provide significant gains 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.