Frontiers and open sets in abstract interpretation
Sebastian Hunt · 1989
interpretationis the name applied to a range of techniques which use non-standard semantics to identify properties of computer programs.The central task in applying these techniques is to find fixed points of recursive definitions.To fulfil this task efficiently, a compact representation of function values is needed.Clack and Peyton Jones showed how sets of incomparable points from a function's argument domain, known as frontiers, could meet this need for function spaces of the form [2" -+ 21.They also developed the frontiers algorithm, a method of establishing the frontier representation of a function.Martin and Bankin extended the method to cope with higherorder functions over more general finite lattices.In this paper we present a new approach to the frontiers algorithm based on the insight that frontiers represent open and closed subsets of a function's argument domain.This insight leads to a new formulation of the frontiers algorithm for higher-order functions over a rich famiIy of finite lattices.This formulation is considerably more concise than previous versions.We go on to argue that for many functions, especially in the higher-order case, finding fixed points is an intractable problem unless the sizes of the abstract domains are reduced.We show how the semantic machinery of abstract interpretation allows us to place upper and lower bounds on the values of fixed points in large lattices by working within smaller ones.