Formal specification and prototyping of a program specializer

Sandrine Blazy 1 Philippe Facon 1
1 CEDRIC - Centre d'Etude et De Recherche en Informatique du Cnam
Abstract : This paper reports on the use of formal specifications in the development of a software maintenance tool for specializing imperative programs, which have become very complex due to extensive modifications. The tool is specified in terms of inference rules and operates by induction on the abstract syntax. The correctness of these rules is proved using rule induction. A Prolog prototype has been derived for Fortran programs, using the Centaur programming environment.
Keywords : structured operational semantics VDM software maintenance program specialization proof of correctness rule induction Centaur
Type de document :
Communication dans un congrès
Springer Verlag. TAPSOFT '95: Theory and Practice of Software Development, 6th International Joint Conference CAAP/FASE, May 1995, Aarhus, Denmark. 915, pp.666-680, Lecture Notes in Computer Science. 〈10.1007/3-540-59293-8_227〉
Liste complète des métadonnées

Littérature citée [8 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00165933
Contributeur : Sandrine Blazy <>
Soumis le : lundi 30 juillet 2007 - 14:41:00
Dernière modification le : dimanche 1 avril 2018 - 10:28:04
Document(s) archivé(s) le : jeudi 8 avril 2010 - 21:04:09

Fichier

fulltext.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Collections

Citation

Sandrine Blazy, Philippe Facon. Formal specification and prototyping of a program specializer. Springer Verlag. TAPSOFT '95: Theory and Practice of Software Development, 6th International Joint Conference CAAP/FASE, May 1995, Aarhus, Denmark. 915, pp.666-680, Lecture Notes in Computer Science. 〈10.1007/3-540-59293-8_227〉. 〈inria-00165933〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

82

Téléchargements de fichiers

97

Contact


archive-ouverte@inria.fr