Algebraic Specification of a Binary Tree

Our next example features the algebraic specification of a familiar data structure, the binary tree. Trees are one of the most important nonlinear structures in computer science. In part, this is due to the fact that they provide natural representations for many kinds of hierarchical and nested data that arise in computer applications. File index schemes and hierarchical data base management systems, for example, often make use of tree structures.

This example of the specification of a binary tree (a tree where each node has no more than two child nodes) will be further explored later when we discuss hidden or private operations. For the binary tree, the operations normally required are

• empty : allocate and initialise the binary tree

• make : operation which takes a data element and two binary trees and constructs a tree with the data element as the root and the two binary trees as left and right subtrees

• left : operation which takes a binary tree and returns the left subtree

• right : operation which takes a binary tree and returns the right subtree

• node : operation which takes a binary tree and returns the value of the data element corresponding to the root of the tree

• is-empty? : operation which returns true if the binary tree is empty and false if the tree is not empty

• is-in? : operation which returns true if a specified data element is present in the tree and returns false if the data element is not present

As with the previous examples, we assume for the sake of expediency, that the data elements are natural numbers. The individual signatures of the operations are then given by

   empty     :  ->  binary-tree
 
   make      :  binary-tree  nat  binary-tree ->  binary-tree

   left      :  binary-tree  ->  binary-tree

   right     :  binary-tree  ->  binary-tree

   node      :  binary-tree  ->  nat

   is-empty? :  binary-tree  ->   bool

   is-in?    :  binary-tree  nat  ->  bool

where binary-tree is the sort introduced by the abstract data type Binary-tree.

The atomic constructors for this abstract data type are empty and make since any binary tree can be constructed using a composition of these two constructors (the operations left and right are non-atomic constructors for this example and such operations are sometimes referred to as ``destructors''). The complete specification is shown in Fig. 9.4. We have introduced the nullary operation nat-error    :     $\rightarrow$    nat to deal with the result of trying to access the value corresponding to the root of an empty tree.

  

Figure 9.4: Algebraic specification for a binary tree