%%% %%% The binary tree data type. Note the parameterization of values. %%% tree[T:TYPE]: DATATYPE BEGIN leaf : leaf? node(val: T, left: tree, right: tree): node? END tree th_L: THEORY BEGIN IMPORTING tree_adt[int] itree: TYPE = tree[int] i,j,k,l,m : VAR int t,rt,lt : VAR itree %%% %%% seek searches a tree depth-first, left-to-right %%% for an occurance of a node containing value i. %%% seek(i:int, tr:itree): RECURSIVE itree = CASES tr OF leaf: tr, node(j, lt, rt): IF (j = i) THEN tr ELSE LET st = seek(i, lt) IN IF leaf?(st) THEN seek(i, rt) ELSE st ENDIF ENDIF ENDCASES MEASURE tr BY << test_tree_1:itree = node(1, node(2, leaf, leaf), node(3, leaf, leaf)) L0: PROPOSITION val(seek(3, test_tree_1)) = 3 %%% %%% This proposition says 'seek' always returns a node with the right value. %%% L1: PROPOSITION (FORALL (i:int, t:itree) : node?(seek(i,t)) => val(seek(i,t)) = i) %%% %%% count the interior nodes in a tree %%% count_nodes(tr:itree): RECURSIVE nat = CASES tr OF leaf: 0, node(j, lt, rt): 1 + count_nodes(lt) + count_nodes(rt) ENDCASES MEASURE tr BY << %%% %%% count the leaves in a tree %%% count_leaves(tr:itree): RECURSIVE nat = CASES tr OF leaf: 1, node(j, lt, rt): count_leaves(lt) + count_leaves(rt) ENDCASES MEASURE tr BY << %%% %%% size(tr) = #nodes + #leaves %%% size_of(tr:itree):nat = count_leaves(tr) + count_nodes(tr) %%% %%% A tree always has exactly one more leaves than nodes. %%% L2: PROPOSITION (FORALL (t:itree) : count_leaves(t) = count_nodes(t) + 1) %%% %%% depth calculates the depth of a tree %%% depth(tr:itree): RECURSIVE nat = CASES tr OF leaf: 1, node(j, lt, rt): 1 + max(depth(lt), depth(rt)) ENDCASES MEASURE tr BY << %%% %%% a FULL tree has uniform depth and balance. %%% full_tree(tr:itree): RECURSIVE bool = CASES tr OF leaf: TRUE, node(j, lt, rt): depth(lt) = depth(rt) AND full_tree(lt) AND full_tree(rt) ENDCASES MEASURE tr BY << %%% %%% The size of a full tree is one less than a power of two %%% l3: PROPOSITION (FORALL (t:itree) : full_tree(t) IMPLIES size_of(t) = 2^(depth(t)) - 1) END th_L