Question#4:   (15)
Defines a binary search tree where the data is of generic type Elem.
Build is an additional primitive constructor operation which is introduced to simplify the specification. It builds a tree given the value of a node and the left and right sub-tree.

Add(Binary_tree, Elem)	Adds a node to the binary tree using the usual ordering principles
Left(Binary_tree)	Returns the left sub-tree of the top of the tree
Data(Binary_tree)	Returns the value of the data element at the top of the tree
Right(Binary_tree)	Returns the right sub-tree of the top of the tree
IsEmpty(Binary_tree)	Returns true of the tree does not contain any elements
Contains(Binary_tree, Elem)	Returns true of the tree contains the given element

Solution:

Signatures

Create => Binary_tree
Add(Binary_tree, Elem) => Binary_tree
Left(Binary_tree) => Binary_tree
Data(Binary_tree) => Elem
Right(Binary_tree) => Binary_tree
IsEmpty(Binary_tree) => Boolean
Contains(Binary_tree, Elem) => Boolean
Build(Binary_tree, Elem, Binary_tree) => Biniary_tree

Axioms

We need to specify a Binary Search Tree,its signature is given below,Write axioms to complete Specification.Write down the Axioms for Binary Search Tree?

Add (Create, E)                    =  Build(Create, E, Create)

Add (B, E)                            =  if E < Data (B) then Add (Left(B), E)

                                                  else Add (Right (B), E)

Left (Create)                      = Create

Right (Create)                    = Create

Data (Create)                     = Undefined

Left (Build(L, D, R))         = L

Right (Build(L, D, R))       = R

Data (Build(L, D, R))        = D

IsEmpty(Create)                = true

IsEmpty (Build (L, D, R)) = false

Contains (Create, E)          = false

Contains (Build (L, D, R), E)           = if E = D then true

                                                             else if  E < D then Contains (L, E)

                                                                          else Contains (R, E)