VDM Specification of an Ordered Binary Tree

It will be of interest to compare the algebraic specification Ordered-tree with its VDM counterpart. A binary tree is a recursive data structure in the sense that the structure consists of either an ``empty'' root node or a root node that has a value together with two further ``branches'' (left and right) which are themselves further instances of the same data structure. In VDM, we can specify such a data structure using a composite which is recursively defined, with an extension of a type definiton method introduced in Chapter 3. Recall that a type can be defined using the bar '|', meaning 'or', for example:

type_nameconstant1 | constant2 | constant3 | constant4

These constants, however, can be generalised to be type names, and this gives us a way of `unioning' types. For example, if we wanted to create a type natural numbers with an error value, we would write:

Nat_error| error

This allows types to be recursively defined, and, but for syntax, is the same as the signature of a constructor operation in an algebraic specification. The VDM binary tree is defined thus:

Ordered_treeOrd_bin_tree | Empty

mk-Ord_bin_tree(l,val,r)
n node_values(l) n < val n node_values(r) n > val

In this definition, we have introduced the function

which retrieves all the node values from an ordered tree and places them in a set. The invariant then states that all natural numbers n that belong to the set of node values returned from the left subtree of the tree with ``val'' as the root must be less than val, and all the numbers returned from the right subtree must be greater than val.

The introduced function $node\_values$ is itself defined recursively by observing that we can construct the set of all node values of a given tree by applying $node\_values$ to the left subtree and the right subtree and taking the union of these two sets with the set {val} where val is the natural number at the root node. The recursion is terminated by noting that applying $node\_values$ to an empty tree will produce the empty set {}. This leads immediately to the definition

We are now ready to model the operations (recall from chapter 5 that operations which are explicitly defined functions have their names written in lower case).