Many semantic analyses of functional languages have been developed using the Cousots’abstract interpretationframework. Some operate onabstract valuesrepresenting the past history of the computation, and are therefore calledforwards analyses. Others propagateabstract contextsrepresenting the future of the computation, and are calledbackwards 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 combine
展开▼
