An experiment in formal software development: using the B theorem prover on a VDM case study
C. Lafontaine, Yves Ledru, Pierre‐Yves Schobbens · Repository of the University of Namur · 1990
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. >