next up previous contents
Next: The VDM Operations and Up: VDM Specification of an Previous: VDM Specification of an

The VDM Operation build

The first operation is build which inserts a number into an ordered tree. This operation must preserve the data type invariant and can be specified thus:


\begin{fn}{build} \signature{Ordered\_tree \X \Nat \To Ordered\_tree} \parms{t,n... ...e(leftsub,value,rightsub) \And n > value \Then\\ build(rightsub,n) \Fi \end{fn}

This algorithm for build will ensure that the data type invariant is satisfied. It is left as an exercise for the reader to show that the invariant is preserved each time a value is inserted into an ordered tree.

Lee McCluskey
2002-12-18