Skip to content
Snippets Groups Projects
Commit 745e763a authored by Viktor Kuncak's avatar Viktor Kuncak
Browse files

BST is great

parent b68c7f90
No related branches found
No related tags found
No related merge requests found
...@@ -60,16 +60,15 @@ object BSTSimpler { ...@@ -60,16 +60,15 @@ object BSTSimpler {
Node(l, v, r) Node(l, v, r)
}) })
} }
// } ensuring (contents(_) == contents(tree) ++ Set(value)) } ensuring(res => isBST(res) && content(res) == content(tree) ++ Set(value))
} ensuring(isBST(_))
def createRoot(v: Int): Node = { def createRoot(v: Int): Node = {
Node(Leaf(), v, Leaf()) Node(Leaf(), v, Leaf())
} ensuring (contents(_) == Set(v)) } ensuring (content(_) == Set(v))
def contents(tree: Tree): Set[Int] = tree match { def content(tree: Tree): Set[Int] = tree match {
case Leaf() => Set.empty[Int] case Leaf() => Set.empty[Int]
case Node(l, v, r) => contents(l) ++ Set(v) ++ contents(r) case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
} }
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment