Specification of Binary Tree

Structure: a binary is either empty or consists of a component value, and optional left and right binary subtrees.

Direction: Left, Right, Up.

Core Operations: CREATE_EMPTY, DESTROY, CREATE_SINGLETON, IS_EMPTY, GET_ROOTVALUE.

GET_TREE

• Input: T1 and D
• Output: T2
• Preconditions: if D = Up, T1 must be a subtree. If D = Left or D = Right, the corresponding subtree must exist.
• Postconditions: T2 is T1's left subtree, right subtree, or parent tree, as specified by D.

GET_TREE is the counterpart to MOVE_FORWARD and MOVE_BACKWARD