|
 
|
[BF95] Formal specification and prorotyping of a program specializer
Conférence Internationale avec comité de lecture : TAPSOFT'95, Aarhus, January 1995, pp.666-680, Series LNCS 915,
motcle:
Résumé:
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.
BibTeX
| @inproceedings { | |||
| BF95, | |||
| title | = | "{Formal specification and prorotyping of a program specializer}", | |
| author | = | " S. Blazy and P. Facon ", | |
| booktitle | = | "{TAPSOFT'95, Aarhus}", | |
| year | = | 1995, | |
| month | = | "January", | |
| series | = | "LNCS 915", | |
| pages | = | "666-680", | |
| } | |||
