A framework for specification and implementation of program analysis algorithms
G. A. Venkatesh, Charles N. Fischer · Minds at UW (University of Wisconsin) · 1989
Program analysis algorithms take a program as input and output information about static and dynamic properties of the program. Flow analysis algorithms form an important class of analysis algorithms and have been used extensively in implementation of programming languages. Recent developments in programming environments have resulted in language-based editors that carry out many tasks that were once traditionally considered as compiler functions. In addition to various flow analysis algorithms, other kinds of program analysis algorithms such as type inference or complexity analysis can be used to provide powerful interactive programming environments. The growing sophistication of these analysis algorithms necessitates a structured approach to their design to ease their development as well as to ensure their correctness. Currently, analysis algorithms are either developed in operational frameworks that make formal verification difficult or specified in theoretical frameworks that do not translate easily into implementations. This thesis bridges the gap between theory and practice by developing a framework to specify program analysis algorithms. The feasibility of the framework is demonstrated by the construction of a tool based on the framework. This thesis: (1) Demonstrates the feasibility of developing a wide variety of analysis algorithms through high-level specifications. (2) Identifies certain characteristics of program analysis algorithms and documents their impact on the design of a denotational specification language. (3) Proposes a specification language with features that allow analysis algorithms to be expressed in a clear and concise fashion. (4) Provides a formal semantics for the specification language. (5) Develops guidelines for deriving correctness proofs for analysis algorithms. (6) Provides a tool that can be used for rapid prototyping of analysis algorithms.