Project Description: Binary Search Trees
Specify a binary-tree search structure for holding integers.
Recall from Homework Assignment L.pvs the inductive
definition of tree type:
tree[T:TYPE]: DATATYPE
BEGIN
leaf : leaf?
node(val: T, left: tree, right: tree): node?
END tree
The goal is to define functions
for inserting items, deleting and
finding items. That is, define functions
- S(n, t) → t (Search) that finds and returns a node with
value n, if tree t contains one,
or the leaf otherwise.
- I(n, t) → t (Insert) inserts a node with value n
in tree t unless it already contains one, returning the
root node of the resulting tree.
- D(n, t) → t (Delete) the node (or all nodes) with value
n from tree t and returns the resulting tree.
The minimal correctness properties of S, I and D are:
- val(S(n, I(n, t))) = n. An inserted value can always be found in the
resulting tree.
- leaf?(S(n, D(n, t))). A deleted value cannot be found in the
resulting tree.
The object is to restrict the trees that these functions operate
on to make searching more efficient, considered as programs.
Ordered Binary Trees (OBT). In an OBT t, b is either the leaf or its nodes are arranged so that:
- val(left(t)) < val(t) < val(right(t)), unless these are leafs.
- left(t) and right(t) are OBTs.
greater than the node's value.
Searching, inserting and deleting values in OBTs is faster because the
functions can always determine which one of the subtrees follow and may
ignore the other. Of course, the insert
and delete operations must preseve the ordered
property of the tree.
Balanced Ordered Binary Trees. BOBTs are
OBTs in which, at any node, the size of the two subtrees
is about the same. BOBTs further minimize the search times
of the operations.
Other Search Tree Structures. P515 students doing this project
might consider formulating other structures, such as Red-Black.
However, in the time given, BOBTs would be a strong outcome for this project.