From c6795423b0465e406829e124259a884a70a2cc8e Mon Sep 17 00:00:00 2001
From: Swen Jacobs <swen.jacobs@epfl.ch>
Date: Tue, 13 Jul 2010 08:25:51 +0000
Subject: [PATCH] corrected postcondition of isSorted
---
testcases/BinarySearchTree.scala | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/testcases/BinarySearchTree.scala b/testcases/BinarySearchTree.scala
index cd2686add..ce313c307 100644
--- a/testcases/BinarySearchTree.scala
+++ b/testcases/BinarySearchTree.scala
@@ -55,7 +55,7 @@ object BinarySearchTree {
}
}
}) ensuring (res => res match { case SortedTriple(min,max,sort) => min match {
- case None() => res == SortedTriple(None(),None(),false)
+ case None() => res == SortedTriple(None(),None(),sort)
case Some(minv) => max match {
case None() => false
case Some(maxv) => sort && minv <= maxv}}})
--
GitLab