Derivation of Static Analysers of Functional Programs From Path Properties of a Natural Semantics
Valérie Gouranton, Daniel Le Métayer, 35 - Rennes (France). Inst. de Recherche en Informatique et Systemes Aleatoires (IRISA) Centre National de la Recherche Scientifique (CNRS), 35 (France). Inst. de Recherche en Informatique et Systemes Aleatoires (IRISA) Rennes-1 Univ., 35 (France). Inst . de Recherche en Informatique et Systemes Aleatoires (IRISA) Institut National des Sciences Appliquees de Rennes (INSA), 35 - Rennes (France). Inst. de Recherche en= Informatique et Systemes Aleatoires (IRISA) Institut National de Recherche en Informatique et en Automatique (INRIA) · 1995
: 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, : : : ) and the mechanical derivation of the corresponding analyses. Key-words: functional languages, operational semantics, neededness analysis, paths analysis, optimising compilers. (R'esum'e : tsvp) [email protected] [email protected] Unite de recherche INRIA Rennes IRISA, Campus universitaire de Beaulieu, 35042 RENNES Cedex (France) Telephone : (33) 99 84 71 00 -- Telecopie : (33) 99 84 71 D'erivation d'analyseurs de programmes fonctionnels `a partir de propri'et'es de chemin d'une s'ema...