VDMPad: a lightweight IDE for exploratory VDM-SL specification

The lightweight use of formal methods is an effective approach to using formal specifications in various phases of software development. This paper proposes tool support specialised for the earlier stages of development that involves incremental and exploratory production of a formal specification. The VDMPad tool is described, as well as its features supporting incremental and exploratory development.