page 1  (22 pages)
2to next section

Backward Analysis

for Higher{Order Functions

Using Inverse Images

Tyng{Ruey Chuang

Benjamin Goldberg

Department of Computer Science

New York University?

February 1991

Abstract

We propose a method for performing backward analysis on higher{order functional programming languages based on computing inverse images of functions over abstract domains. This method can be viewed as abstract interpretation done backward. Given an abstract semantics which supports forward analysis, we can transform it into an abstract semantics which performs backward analysis. We show that if the original abstract semantics is correct and computable, then the transformed version of the abstract semantics is also correct and computable.

More specifically, given a forward abstract semantics of a higher{order functional language which is expressed in terms of Scott{closed powerdomains, we derive an backward abstraction semantics which is expressed in terms of Scott{open powerdomains. The derivation is shown to be correct and the relationships between forward analysis and backward analysis is established.

We apply this method to the classic strictness analysis in functional languages and obtain promising results. We show that the time complexity of inverse image based backward analysis is not much worse than the forward analysis from which it is derived. We then compare this work with previous works of Wadler and Hughes [17], Hughes [11], and Burn [5], showing that some special restrictions and constructions in previous works have natural interpretation in the Scott{closed/Scott{open powerdomain framework. A brief outline of applying the inverse image method to other backward semantics analysis is also given.

?The authors' address: Department of Computer Science, Courant Institute of Mathematical Sciences, New York University, 251 Mercer Street, New York, NY 10012, USA. E{mail: chuang@cs.nyu.edu, goldberg@cs.nyu.edu. This paper is available as Technical Report 620 from the Department of Computer Science, New York University, at the above address. An electronic version is also available from the ftp site cs.nyu.edu. This research has been supported, in part, by the National Science Foundation (#CCR{8909634) and DARPA (DARPA/ONR #N00014{91{J1472).