Introduction

In the glossary of terms in his book [J90] Cliff Jones explains the origin of the name Vienna Development Method.

VDM is the name given to a collection of notation and concepts which grew out of the work of the IBM Laboratory, Vienna. The original application was the denotational description of programming languages. The same specification technique has been applied to many other systems. Design rules which show how to prove that a design satisfies its specification have been developed. [J90, p. 294]

Of the techniques mentioned above, Bicarregui et al [BFL+94] stress three as the main ones: the specification language VDM-SL, data refinement techniques, and operation decomposition techniques, where the latter term refers to refinement as opposed to data refinement, for instance, the implementation of a specification statement by a loop.

One keyword in the quote above is ‘rule’. Nowadays the first impression a student might get when learning and practising VDM is that of a huge collection of rules to guide writing specifications. Indeed, specifying with VDM mostly comprises two activities carried out together:

• writing specifications of, e.g., types, functions, and operations in the specification language and

• discarding proof obligations — preferably by formal proof — that ensure, for instance, that a type1 is nonempty, a function specification is well-formed, a specification of an operation is satisfiable, or a specification is implemented by an operation.

• Of course, we focus in this monograph on the proof obligations that arise in the process of data refinement.