Title :
An experiment in formal software development: using the B theorem prover on a VDM case study
Author :
Lafontaine, Christine ; Ledru, Yves ; Schobbens, Pierre-Yves
Author_Institution :
Univ. Catholique de Louvain, Belgium
Abstract :
The authors give a short overview of the B theorem prover and report on its experimental evaluation. They describe the application of B to control VDM developments and illustrate this by means of excerpts from a case study. This work results in a formal description of the logical framework of VDM and opens perspectives for the reuse of software developments
Keywords :
program verification; software engineering; software reusability; theorem proving; B theorem prover; VDM case study; experimental evaluation; formal description; formal software development; logical framework; reuse; Application software; Artificial intelligence; Computer aided software engineering; Design engineering; Hardware; Large-scale systems; Logic; Programming; Software engineering; Software tools;
Conference_Titel :
Software Engineering, 1990. Proceedings., 12th International Conference on
Conference_Location :
Nice
Print_ISBN :
0-8186-2026-9
DOI :
10.1109/ICSE.1990.63601
