Skip to content
Snippets Groups Projects
Commit d6b502c5 authored by Swen Jacobs's avatar Swen Jacobs
Browse files

added/uncommented postconditions in MergeSort.scala and QuickSort.scala,\n...

 added/uncommented postconditions in MergeSort.scala and QuickSort.scala,\n added range restrictions as postcondition of isSorted in BinarySearchTree.scala
parent b6ecd84a
No related branches found
No related tags found
No related merge requests found
......@@ -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)
......
......@@ -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))
}
......
......@@ -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()))))))
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment