Software tools for VDM

The authors describe a tool set developed to assist the construction of specifications using the Vienna Development Method (VDM). It includes syntax and semantic checkers, a lemma generator and a proof checker. The aim of the project was not to develop a highly efficient toolset with a sophisticated user interface. Rather, emphasis was placed on quickly producing a complete system. This approach allowed the authors to proceed quickly to the specification and construction of the proof checker, the most interesting and challenging of the components