diff --git a/testcases/BinarySearchTree.scala b/testcases/BinarySearchTree.scala
index 1db8dcd109c59aa0539958a7c247f5b768528c0a..cd2686addcf9d5ad472d977644a1d537aa66e124 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 4dd8a2793d9abbc7d558f2f0110f990c13d5be07..da575c8bb2cc8c5df6d32a0ec066c4d19cc4e6f9 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 a4cb93be2a8cf01a9cccadb236e9e5fa7b813821..030ff9e626f5881733fa3222109e8af3117e358e 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()))))))