Formal development of static program analysers
Valérie Gouranton, Daniel Le Métayer · 2002
We propose an approach for the formal development of static analysers which is based on transformations of inference systems. The specification of an analyser is made of two components: an operational semantics of the programming language and the definition of a property by recurrence on the proof trees of the operational semantics. The derivation is a succession of specialisations of inference systems with respect to properties on their proof trees. In this paper we illustrate the methodology with the derivation of analysers for a non-strict functional language.