Abstract interpretation using domain theory
Flemming Nielson · ERA · 1984
A framework is developed for describing and proving the correctness of certain data flow analyses. This is done by ascribing several semantics to the programming language studied. The standard semantics is the usual semantics and an approximating semantics describes a data flow analysis. A value in the latter somantics describes a set of values in the former and this is expressed using the framework of abstract interpretation pioneered by P. and R. Cousot. Their view of a programming language is limited because a program is viewed as a (kind of) flowchart and the main aim of this work therefore is to extend the framework to all programming languages that have a denotational semantics. This is accomplished except for "storable procedures". A secondary aim is to extend abstract interpretation to include certain aspects of termination. The first aim is addressed by studying a metalanguage for denotational semantics. A collecting semantics is defined and it may be viewed. as the most precise of all data flow analyses. Its formulation requires a study of (relational) powerdomains. It is then proved correct and "as precise as possible" wi th respect to the standard semantics. The development of abstract interpretation generalises the previous approaches. In particular, the tensor product is found to generalise the relational method just as cartesian product corresponds to the independent attribute method. It is studied how to pass between such methods and how func tionals like conditional are likely to look. To achieve the second aim another powerdomain is required. The development of abstract interpretation distinguishes between two partial orders: E is the usual partial order of denotational semantics and !E expresses the data flow analysis idea of "safe approximation". (It was-E- above. ) An example is given that requires this framework. Another example studie's a nondeterministic language and its usual (nondeterministic) denotational semantics. It is shown that the semantics may be viewed as a data flow analysis upon a deterministic language where oracles resolve the choice of paths. This view motivates the definition of a nondeterministic denotational semantics that distinguishes between "may diverge" and "may have to diverge".