Higher Order Strictness Analysis by Abstract Interpretation Over Finite Domains

A construction for finite abstract domains is presented which is quite general, being applicable to any algebraic data type, including higher order cases, based on the notion of a 'set of elements'. This generalises earlier work on the abstract interpretation of lazy lists. The abstraction for elements is given, and a new powerdomain is developed. Then a means of iterative calculation of the sub-domain which contains all the 'useful' points is arrived at, and abstractions for the constructors and case-expressions are derived. An implementation of higher-order strictness analysis by abstract interpretation is described, which uses techniques taken from work on the semantics of sequential programming languages. Using sequential algorithms, we are able to calculate portions of least fixed points of abstract functions without the need to evaluate all of some representation of the fixpoint over the entire argument domain. In this sense we claim that our method generalises minimal function graphs to the higher-order case. We consider forwards analysis, using Wadler's domain for lists, but argue that the technique is quite general. Based on our initial results, analysis is much faster than with the frontiers method, the best comparable means known to date