Title :
Formal development of static program analysers
Author :
Gouranton, Valeérie ; Le Metayer, Daniel
Author_Institution :
Inst. Nat. de Recherche en Inf. et Autom., Rennes, France
Abstract :
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
Keywords :
formal specification; functional languages; functional programming; inference mechanisms; program diagnostics; trees (mathematics); formal development; inference systems; methodology; nonstrict functional language; operational semantics; programming language; proof trees; specification; static program analysers; transformations; Algorithm design and analysis; Application software; Computer languages; Debugging; Engineering management; Filtering; Logic programming; Optimizing compilers; Software engineering; Software maintenance;
Conference_Titel :
Computer Systems and Software Engineering, 1997., Proceedings of the Eighth Israeli Conference on
Conference_Location :
Herzliya
Print_ISBN :
0-8186-8135-7
DOI :
10.1109/ICCSSE.1997.599881
