From 6fa8978c26c2da47314aa960d4b0bd2735388de9 Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <vkuncak@gmail.com>
Date: Fri, 9 Jul 2010 15:49:21 +0000
Subject: [PATCH] stronger post in one example
---
testcases/BinarySearchTree.scala | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/testcases/BinarySearchTree.scala b/testcases/BinarySearchTree.scala
index 4d5818dda..617749916 100644
--- a/testcases/BinarySearchTree.scala
+++ b/testcases/BinarySearchTree.scala
@@ -63,7 +63,7 @@ object BinarySearchTree {
} else {
n
}
- }) ensuring(contents(_) != Set.empty[Int])
+ }) ensuring (contents(_) == contents(tree) ++ Set(value))
def contains(tree: Tree, value: Int) : Boolean = tree match {
case Leaf() => false
--
GitLab