Specbox: a toolkit for BSI-VDM

The widespread adoption of mathematically formal methods for software production has been greatly hampered by the lack of tool support. In order to address this deficiency, Adelard has produced a tool to assist with the production of specifications written in VDM (the Vienna development method). Known as SpecBox, the tool provides machine support for the standard BSI-VDM notation. It checks specifications for conformance to the syntax contained in the latest working draft of the BSI-VDM standardisation committee and also identifies certain classes of semantic error. The implementation involves a number of advanced techniques and algorithms to enable it to work effectively on both large and small computer systems. The authors identify the tools required in rigorous and formal software development and introduce BSI-VDM. SpecBox is discussed in detail, providing an outline of the functions it provides, its method of working and the various reports it produces. The authors conclude by considering various enhancements that are planned for SpecBox