diff --git a/testcases/BSTSimpler.scala b/testcases/BSTSimpler.scala index 02957dcbd7fbb45f24870652ae6d627821d48097..f3b2b6893b2658e8ec1c3bcf040abc69a56e62b5 100644 --- a/testcases/BSTSimpler.scala +++ b/testcases/BSTSimpler.scala @@ -49,7 +49,7 @@ object BSTSimpler { def emptySet(): Tree = Leaf() def insert(tree: Tree, value: Int): Node = { - require(size(tree) <= 1 && isBST(tree)) + require(isBST(tree)) tree match { case Leaf() => Node(Leaf(), value, Leaf()) case Node(l, v, r) => (if (v < value) { @@ -62,6 +62,22 @@ object BSTSimpler { } } ensuring(res => isBST(res) && content(res) == content(tree) ++ Set(value)) +/* + def remove(tree : Tree, value : Int) : Tree = { + require(size(tree) <= 1 && isBST(tree)) + tree match { + case Leaf() => Node(Leaf(), value, Leaf()) + case Node(l, v, r) => (if (v < value) { + Node(l, v, insert(r, value)) + } else if (v > value) { + Node(insert(l, value), v, r) + } else { + Node(l, v, r) + }) + } + } +*/ + def createRoot(v: Int): Node = { Node(Leaf(), v, Leaf()) } ensuring (content(_) == Set(v))