From 07731442f4305a4a5fed1c731fd63b3e4987162a Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 15 Oct 2012 18:38:44 +0200
Subject: [PATCH] Add some stuff
---
testcases/SortedTree.scala | 24 ++++++++++++------------
1 file changed, 12 insertions(+), 12 deletions(-)
diff --git a/testcases/SortedTree.scala b/testcases/SortedTree.scala
index 3b69626ec..fcf05dfac 100644
--- a/testcases/SortedTree.scala
+++ b/testcases/SortedTree.scala
@@ -54,7 +54,7 @@ object SortedTree {
v < max &&
v > min
case _ => true
- })
+ }) ensuring ( res => !res || (allGreaterThan(t, min) && allSmallerThan(t, max)))
def isSortedMin(t: Tree, min: Int): Boolean = (t match {
case Node(v, l, r) =>
@@ -62,7 +62,7 @@ object SortedTree {
isSortedMin(r, v) &&
v > min
case _ => true
- })
+ }) ensuring ( res => !res || allGreaterThan(t, min))
def isSortedMax(t: Tree, max: Int): Boolean = (t match {
case Node(v, l, r) =>
@@ -70,7 +70,7 @@ object SortedTree {
isSortedMinMax(r, v, max) &&
v < max
case _ => true
- })
+ }) ensuring ( res => !res || allSmallerThan(t, max))
def isSorted(t: Tree): Boolean = (t match {
case Node(v, l, r) =>
@@ -79,8 +79,8 @@ object SortedTree {
case _ => true
}) ensuring ( res => !res || (t match {
case Node(v, l, r) =>
- allSmallerThan(l, v) &&
- allGreaterThan(r, v)
+ isSorted(l) &&
+ isSorted(r)
case Leaf() => true
}))
@@ -161,7 +161,7 @@ object SortedTree {
(v == searchV) ||
contains1(l, searchV) ||
contains1(r, searchV)
- }) ensuring(res => !res || (content(t) contains searchV))
+ }) ensuring(_ == (content(t) contains searchV))
def contains2(t: Tree, searchV: Int): Boolean = {
require(isMostlySorted(t))
@@ -176,20 +176,20 @@ object SortedTree {
} else {
true
}
- })} ensuring(res => !res || (content(t) contains searchV))
+ })} ensuring(_ == (content(t) contains searchV))
- def containsBuggy(t: Tree, searchV: Int): Boolean = {
- require(isMostlySorted(t))
+ def contains3(t: Tree, searchV: Int): Boolean = {
+ require(isSorted(t))
(t match {
case Leaf() => false
case Node(v, l, r) =>
if (searchV > v) {
- contains2(l, searchV)
+ contains3(r, searchV)
} else if (searchV < v) {
- contains2(r, searchV)
+ contains3(l, searchV)
} else {
true
}
- })} ensuring(res => !res || (content(t) contains searchV))
+ })} ensuring(_ == (content(t) contains searchV))
}
--
GitLab