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

fYear

1997

fDate

18-19 Jun 1997

Firstpage

101

Lastpage

110

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Systems and Software Engineering, 1997., Proceedings of the Eighth Israeli Conference on

Conference_Location

Herzliya

Print_ISBN

0-8186-8135-7

Type

conf

DOI

10.1109/ICCSSE.1997.599881

Filename

599881