A Deep Dive into VDM

VDM (the Vienna Development Method) is one of the longest-established model-oriented formal methods, with roots in programming-language semantics research at IBM's Vienna Laboratory in the 1970s. Its specification language VDM-SL is an ISO standard (ISO/IEC 13817-1:1996), and the method has grown into VDM++ (object-oriented) and VDM-RT (distributed, real-time).

VDM's great practical strength is that specifications can also be written in an executable form. While mathematically rigorous, a specification written in the executable style (the explicit style introduced below) can be run in an interpreter to observe its behavior (specification animation), so errors in the specification itself can be found before any implementation exists. Industrial track records include large-scale IC-card firmware development in Japan.

Representative tools: Overture (IDE), VDMJ (command-line processor), ViennaTalk

"Sort a list into ascending order" — what happens when we write this familiar operation as a formal specification? The crucial point is that the specification of sorting never mentions the algorithm — neither merge sort nor quicksort appears anywhere. What a specification must define is exactly one thing: for a given input, what output is acceptable.

In VDM, this "what output is acceptable" is written as a postcondition. Defining a function only by its pre- and postconditions, with no body (no algorithm), is called an implicit specification — the fundamental style of specification in VDM.

In words: "Sort takes a sequence of integers l and returns a sequence of integers r, such that r is a permutation of l and r is in ascending order." That is the entire specification of sorting. Note that there is no precondition (pre) — every sequence of integers is acceptable as input.

The two predicates in the postcondition are themselves defined as VDM functions. IsOrdered states that a later element is never smaller than an earlier one (ascending order); IsPermutation states that every value occurs the same number of times in both sequences — the output is a rearrangement of the input.

A VDM function can be written in two styles: an implicit specification, which fixes only the properties to satisfy via pre- and postconditions, and an explicit specification, which supplies a body (a way to compute). Development typically starts by pinning down the properties implicitly, then refines step by step toward explicit definitions and implementations.

VDM also lets you keep the explicit form while leaving the body undefined, using "is not yet specified". This records that a function's contents are deliberately not decided yet, in a form that still type-checks.

The official Overture example "sort" (Peter Gorm Larsen, 2010) collects several explicit specifications of the same sorting problem. All of them are executable — and all of them satisfy the postcondition of the implicit specification above.

1. Running the specification (almost) as-is: choose a sorted permutation

"From the permutations of l, pick one that is ordered" — an explicit specification that mirrors the structure of the postcondition, written with the nondeterministic choice let ... be st ... (choose one such that). Permutations is an auxiliary function returning the set of all permutations of l (definition omitted). With n! permutations it is far too slow for practical use, but it shows what the halfway point between a specification and an implementation looks like.

2. Insertion sort

A recursive definition: sort the tail, then insert the head element at its correct position.

3. Merge sort

A divide-and-conquer definition: split the list roughly in half, sort each part, and merge them. Note let ... be st ... appearing again — this time to "choose a split whose length difference is less than 2".

Running it

Explicit specifications run as-is in the VDMJ / Overture interpreter. You can observe behavior at the specification stage, before writing any implementation — this is specification animation.

A postcondition is not mere documentation — it is a verification device. In VDM the same pre- and postconditions can also be attached to an explicit definition, and VDMJ checks them automatically at runtime — so if an explicit specification (or an implementation derived from it) violates the properties, the violation is caught on the spot.

Moreover, the question "does this explicit specification really satisfy the postcondition?" can itself be generated mechanically as a proof obligation and then proved. Execution and testing can only show correctness for the inputs you tried; a proof guarantees correctness for all inputs.