From 9ff7ddd11d3febf7a6ae6db381edd7905fe11d23 Mon Sep 17 00:00:00 2001
From: Utkarsh Upadhyay <musically.ut@gmail.com>
Date: Mon, 12 Jul 2010 17:32:19 +0000
Subject: [PATCH] Thanks to Swen's isSorted function, contains can be
successfully verified.
---
testcases/BinarySearchTree.scala | 11 ++++++-----
1 file changed, 6 insertions(+), 5 deletions(-)
diff --git a/testcases/BinarySearchTree.scala b/testcases/BinarySearchTree.scala
index 396678886..c2e4566f4 100644
--- a/testcases/BinarySearchTree.scala
+++ b/testcases/BinarySearchTree.scala
@@ -1,5 +1,5 @@
import scala.collection.immutable.Set
-import scala.collection.immutable.Multiset
+// import scala.collection.immutable.Multiset
object BinarySearchTree {
sealed abstract class Tree
@@ -15,8 +15,7 @@ object BinarySearchTree {
sealed abstract class Triple
case class SortedTriple(min: Option, max: Option, sorted: Boolean) extends Triple
-
- def isSorted(tree: Tree): SortedTriple = tree match {
+ def isSorted(tree: Tree): SortedTriple = tree match {
case Leaf() => SortedTriple(None(), None(), true)
case Node(l,v,r) => isSorted(l) match {
case SortedTriple(minl,maxl,sortl) => if (!sortl) SortedTriple(None(), None(), false)
@@ -140,7 +139,9 @@ object BinarySearchTree {
res.left != Leaf() && res.right != Leaf()
)
- def contains(tree: Tree, value: Int): Boolean = tree match {
+ def contains(tree: Tree, value: Int): Boolean = {
+ require(isSorted(tree).sorted)
+ tree match {
case Leaf() => false
case n@Node(l, v, r) => if (v < value) {
contains(r, value)
@@ -149,7 +150,7 @@ object BinarySearchTree {
} else {
true
}
- }
+ } } ensuring( _ || !(contents(tree) == contents(tree) ++ Set(value)))
def contents(tree: Tree): Set[Int] = tree match {
case Leaf() => Set.empty[Int]
--
GitLab