© 1992 by Oxford University Press
Original Articles |
Relational Reversal of Abstract Interpretation
Department of Computing Science, University of Glasgow UK.rjmhjl{at}dcs.glasgow.ac.uk
Many semantic analyses of functional languages have been developed using the Cousots’ abstract interpretation framework. Some operate on abstract values representing the past history of the computation, and are therefore called forwards analyses. Others propagate abstract contexts representing the future of the computation, and are called backwards analyses. Each form of analysis brings its own insights, and has the potential to influence the other form. For example, it may be very easy to see how to analyse a particular programming language construct in one direction, but not in the direction needed for a particular analysis. Potentially, one might be able to draw on the given analysis to aid in the Resign of a corresponding reversal. This is the topic of this paper. We show how to reverse any given analysis (forwards or backwards), obtaining a relational reversal which is equivalent to the original. This allows the accuracy of two analyses originally defined in opposite directions to be compared directly. Furthermore, we demonstrate that the relational reversal may be safely approximated by a (more-efficient but slighly less accurate) locally-relational analysis. That is, relational and non-relational reversals may be combined.