From d6b502c56f7d1211ee6435cc5d5046de67165bc1 Mon Sep 17 00:00:00 2001
From: Swen Jacobs <swen.jacobs@epfl.ch>
Date: Tue, 13 Jul 2010 08:17:38 +0000
Subject: [PATCH] added/uncommented postconditions in MergeSort.scala and
QuickSort.scala,\n added range restrictions as postcondition of isSorted in
BinarySearchTree.scala
---
testcases/BinarySearchTree.scala | 8 ++++++--
testcases/MergeSort.scala | 23 ++++++++++++-----------
testcases/QuickSort.scala | 4 ++--
3 files changed, 20 insertions(+), 15 deletions(-)
diff --git a/testcases/BinarySearchTree.scala b/testcases/BinarySearchTree.scala
index 1db8dcd10..cd2686add 100644
--- a/testcases/BinarySearchTree.scala
+++ b/testcases/BinarySearchTree.scala
@@ -15,7 +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)
@@ -54,7 +54,11 @@ object BinarySearchTree {
}
}
}
- }
+ }) ensuring (res => res match { case SortedTriple(min,max,sort) => min match {
+ case None() => res == SortedTriple(None(),None(),false)
+ case Some(minv) => max match {
+ case None() => false
+ case Some(maxv) => sort && minv <= maxv}}})
def treeMin(tree: Node): Int = {
require(isSorted(tree).sorted)
diff --git a/testcases/MergeSort.scala b/testcases/MergeSort.scala
index 4dd8a2793..da575c8bb 100644
--- a/testcases/MergeSort.scala
+++ b/testcases/MergeSort.scala
@@ -35,15 +35,7 @@ object MergeSort {
def split(list:List,n:Int): Pair = splithelper(Nil(),list,n)
- def mergeSort(list:List):List = list match {
- case Nil() => list
- case Cons(x,Nil()) => list
- case _ =>
- val p = split(list,length(list)/2)
- merge(mergeSort(p.fst), mergeSort(p.snd))
- } //ensuring(res => contents(res) == contents(list) && is_sorted(res))
-
- def merge(aList:List, bList:List):List = bList match {
+ def merge(aList:List, bList:List):List = (bList match {
case Nil() => aList
case Cons(x,xs) =>
aList match {
@@ -54,11 +46,20 @@ object MergeSort {
else
Cons(x,merge(aList, xs))
}
- } //ensuring(res => contents(res) == contents(aList) ++ contents(bList))
+ }) ensuring(res => contents(res) == contents(aList) ++ contents(bList))
+
+ def mergeSort(list:List):List = (list match {
+ case Nil() => list
+ case Cons(x,Nil()) => list
+ case _ =>
+ val p = split(list,length(list)/2)
+ merge(mergeSort(p.fst), mergeSort(p.snd))
+ }) ensuring(res => contents(res) == contents(list) && is_sorted(res))
+
def main(args: Array[String]): Unit = {
val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
-
+
println(ls)
println(mergeSort(ls))
}
diff --git a/testcases/QuickSort.scala b/testcases/QuickSort.scala
index a4cb93be2..030ff9e62 100644
--- a/testcases/QuickSort.scala
+++ b/testcases/QuickSort.scala
@@ -43,11 +43,11 @@ object QuickSort {
case Cons(x,xs) => if (n==x) Cons(x,equals(n,xs)) else equals(n,xs)
}
- def quickSort(list:List): List = list match {
+ def quickSort(list:List): List = (list match {
case Nil() => Nil()
case Cons(x,Nil()) => list
case Cons(x,xs) => append(append(quickSort(smaller(x,xs)),Cons(x,equals(x,xs))),quickSort(greater(x,xs)))
- }//ensuring(res => contents(res) == contents(list) && is_sorted(res))
+ }) ensuring(res => contents(res) == contents(list) && is_sorted(res))
def main(args: Array[String]): Unit = {
val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
--
GitLab