Formalising Methods: An Experiment with VDM and B
Yves Ledru, P-Y. Schobbens · Australian Software Engineering Conference · 1990
This paper reports on an experiment in the formalisation of software development methods and their support by generic tools. Here, the VDM method for rigorous software development has been formalised, and this formalisation has been fed into the B generic theorem prover. Case studies have been developed in this setting. This experiment provided lessons about method formalisation, about VDM in particular, and about the practical limitations of theorem proving tools.