load list-nat1.maude fmod BINTREE-NAT1 is protecting BOOLEAN . protecting NAT1 . protecting LIST-NAT1 . sort BinTree . op empty : -> BinTree [ctor] . op bintree : BinTree Nat BinTree -> BinTree [ctor] . ops preorder inorder postorder : BinTree -> List . ops size weight : BinTree -> Nat . op isSearchTree : BinTree -> Boolean . op reverse : BinTree -> BinTree . vars BT BT' : BinTree . vars N N' : Nat . eq preorder(empty) = nil . eq preorder(bintree(BT, N, BT')) = insertFront(N, *** Root first, then left and right subtrees: concat(preorder(BT), preorder(BT'))) . eq inorder(empty) = nil . eq inorder(bintree(BT, N, BT')) = concat((inorder(BT) N), inorder(BT')) . eq postorder(empty) = nil . eq postorder(bintree(BT, N, BT')) = concat(postorder(BT), (postorder(BT') N)) . eq size(empty) = 0 . eq size(bintree(BT, N, BT')) = s(0) + (size(BT) + size(BT')) . eq weight(empty) = 0 . eq weight(bintree(BT, N, BT')) = N + (weight(BT) + weight(BT')) . eq isSearchTree(BT) = isSorted(inorder(BT)) . eq reverse(empty) = empty . eq reverse(bintree(BT, N, BT')) = bintree(reverse(BT'), N, reverse(BT)) . endfm *** Define some trees to test: fmod TEST-BINTREE-NAT1 is protecting BINTREE-NAT1 . ops tree1 tree2 : -> BinTree . *** The first one corresponds to one in book eq tree1 = bintree( bintree(empty, s(s(0)), bintree(empty, s(s(s(0))), empty)), s(s(s(s(0)))), bintree( bintree(empty, s(s(s(s(s(s(0)))))), empty), s(s(s(s(s(s(s(0))))))), bintree(empty, s(s(s(s(s(s(s(s(s(0))))))))), empty))) . eq tree2 = bintree( bintree(empty, s(s(0)), bintree(empty, s(s(s(0))), empty)), s(s(s(s(0)))), bintree( bintree(empty, s(s(s(s(s(s(0)))))), empty), s(s(s(s(s(0))))), bintree(empty, s(s(s(s(s(s(s(s(s(0))))))))), empty))) . endfm red preorder(tree1) . red inorder(tree1) . red postorder(tree1) . red size(tree1) . red weight(tree1) . red isSearchTree(tree1) . red isSearchTree(tree2) . red reverse(tree1) . fmod SEARCH-TREE is including TEST-BINTREE-NAT1 . sort BinSearchTree . subsort BinSearchTree < BinTree . var BT : BinTree . vars N N2 : Nat . vars BST1 BST2 : BinSearchTree . cmb BT : BinSearchTree if isSearchTree(BT) = true . op insertSorted : BinSearchTree Nat -> BinSearchTree . eq insertSorted(empty, N) = bintree(empty, N, empty) . ceq insertSorted(bintree(BST1, N, BST2), N2) = bintree(insertSorted(BST1, N2), N, BST2) if N2 <= N = true . ceq insertSorted(bintree(BST1, N, BST2), N2) = bintree(BST1, N, insertSorted(BST2, N2)) if N < N2 = true . endfm red tree1 . red tree2 . red insertSorted(tree1, s(0)) .