Derivation of Static Analysers of Functional Programs from Path Properties of a Natural Semantics
Résumé
We advocate the use of operational semantics as a basis for specifying program analyses for functional languages. We put forward a methodology for defining a static analysis by successive refinements of the natural semantics of the language. We use paths as the abstract representation of proof trees and we provide a language for defining properties in terms of recurrence equations on paths. We show the specification of several standard properties on paths (neededness, absence, uniqueness, \ldots) and the mechanical derivation of the corresponding analyses