Derivation of Static Analysers of Functional Programs from Path Properties of a Natural Semantics

Valérie Gouranton 1 Daniel Le Métayer 1
1 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : 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
Type de document :
Rapport
[Research Report] RR-2607, INRIA. 1995
Liste complète des métadonnées

https://hal.inria.fr/inria-00074078
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 14:26:55
Dernière modification le : mercredi 21 février 2018 - 01:51:23
Document(s) archivé(s) le : lundi 5 avril 2010 - 00:04:36

Fichiers

Identifiants

  • HAL Id : inria-00074078, version 1

Collections

Citation

Valérie Gouranton, Daniel Le Métayer. Derivation of Static Analysers of Functional Programs from Path Properties of a Natural Semantics. [Research Report] RR-2607, INRIA. 1995. 〈inria-00074078〉

Partager

Métriques

Consultations de la notice

152

Téléchargements de fichiers

116