Copying sorting and RB tree examples from testcases

pldi2011-testcases/InsertionSort.scala

+import scala.collection.immutable.Set
+import funcheck.Utils._
+
+object InsertionSort {
+  sealed abstract class List
+  case class Cons(head:Int,tail:List) extends List
+  case class Nil() extends List
+
+  sealed abstract class OptInt
+  case class Some(value: Int) extends OptInt
+  case class None() extends OptInt
+
+  def size(l : List) : Int = (l match {
+    case Nil() => 0
+    case Cons(_, xs) => 1 + size(xs)
+  }) ensuring(_ >= 0)
+
+  def contents(l: List): Set[Int] = l match {
+    case Nil() => Set.empty
+    case Cons(x,xs) => contents(xs) ++ Set(x)
+  }
+
+  def min(l : List) : OptInt = l match {
+    case Nil() => None()
+    case Cons(x, xs) => min(xs) match {
+      case None() => Some(x)
+      case Some(x2) => if(x < x2) Some(x) else Some(x2)
+    }
+  }
+
+  def minProp0(l : List) : Boolean = (l match {
+    case Nil() => true
+    case c @ Cons(x, xs) => min(c) match {
+      case None() => false
+      case Some(m) => x >= m
+    }
+  }) holds
+
+  def minProp1(l : List) : Boolean = {
+    require(isSorted(l) && size(l) <= 5)
+    l match {
+      case Nil() => true
+      case c @ Cons(x, xs) => min(c) match {
+        case None() => false
+        case Some(m) => x == m
+      }
+    }
+  } holds
+
+  def isSorted(l: List): Boolean = l match {
+    case Nil() => true
+    case Cons(x, Nil()) => true
+    case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
+  }   
+
+//  def sortedInsInduct0(e: Int, l: List) : List = {
+//    require(l == Nil())
+//    l match {
+//      case Nil() => Cons(e,Nil())
+//      case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
+//    } 
+//  } ensuring(res => isSorted(res))
+//
+//  def sortedInsInduct1(e: Int, l: List) : List = {
+//    require(
+//      isSorted(l) &&
+//      (l match {
+//        case Nil() => false
+//        case Cons(x,xs) => isSorted(sortedIns(e,xs))
+//       })
+//     )
+//
+//    l match {
+//      case Nil() => Cons(e,Nil())
+//      case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
+//    } 
+//  } ensuring(res => isSorted(res))
+
+  def sortedIns(e: Int, l: List): List = {
+    require(isSorted(l) && size(l) <= 5)
+    l match {
+      case Nil() => Cons(e,Nil())
+      case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
+    } 
+  } ensuring(res => contents(res) == contents(l) ++ Set(e) && isSorted(res))
+
+  def sort(l: List): List = (l match {
+    case Nil() => Nil()
+    case Cons(x,xs) => sortedIns(x, sort(xs))
+  }) ensuring(res => contents(res) == contents(l) && isSorted(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(sort(ls))
+  }
+}

pldi2011-testcases/MergeSort.scala

+import scala.collection.immutable.Set
+
+object MergeSort {
+  sealed abstract class List
+  case class Cons(head:Int,tail:List) extends List
+  case class Nil() extends List
+
+  case class Pair(fst:List,snd:List)
+
+  def contents(l: List): Set[Int] = l match {
+    case Nil() => Set.empty
+    case Cons(x,xs) => contents(xs) ++ Set(x)
+  }
+
+  def is_sorted(l: List): Boolean = l match {
+    case Nil() => true
+    case Cons(x,xs) => xs match {
+      case Nil() => true
+      case Cons(y, ys) => x <= y && is_sorted(Cons(y, ys))
+    }
+  }    
+
+  def length(list:List): Int = list match {
+    case Nil() => 0
+    case Cons(x,xs) => 1 + length(xs)
+  }
+
+  def splithelper(aList:List,bList:List,n:Int): Pair = 
+    if (n <= 0) Pair(aList,bList)
+    else
+	bList match {
+    	      case Nil() => Pair(aList,bList)
+    	      case Cons(x,xs) => splithelper(Cons(x,aList),xs,n-1)
+	}
+
+  def split(list:List,n:Int): Pair = splithelper(Nil(),list,n)
+
+  def merge(aList:List, bList:List):List = (bList match {       
+    case Nil() => aList
+    case Cons(x,xs) =>
+    	 aList match {
+   	       case Nil() => bList
+   	       case Cons(y,ys) =>
+    	        if (y < x)
+    		   Cons(y,merge(ys, bList))
+     		else
+		   Cons(x,merge(aList, xs))               
+   	 }   
+  }) 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))
+  }
+}

pldi2011-testcases/QuickSort.scala

+import scala.collection.immutable.Set
+
+object QuickSort {
+  sealed abstract class List
+  case class Cons(head:Int,tail:List) extends List
+  case class Nil() extends List
+
+  def contents(l: List): Set[Int] = l match {
+    case Nil() => Set.empty
+    case Cons(x,xs) => contents(xs) ++ Set(x)
+  }
+
+  def is_sorted(l: List): Boolean = l match {
+    case Nil() => true
+    case Cons(x,Nil()) => true
+    case Cons(x,Cons(y,xs)) => x<=y && is_sorted(Cons(y,xs))
+  }
+
+  def rev_append(aList:List,bList:List): List = aList match {
+    case Nil() => bList
+    case Cons(x,xs) => rev_append(xs,Cons(x,bList))
+  }
+
+  def reverse(list:List): List = rev_append(list,Nil())
+
+  def append(aList:List,bList:List): List = aList match {
+    case Nil() => bList
+    case _ => rev_append(reverse(aList),bList)
+  }
+  
+  def greater(n:Int,list:List) : List = list match {
+    case Nil() => Nil()
+    case Cons(x,xs) => if (n < x) Cons(x,greater(n,xs)) else greater(n,xs)
+  }
+
+  def smaller(n:Int,list:List) : List = list match {
+    case Nil() => Nil()
+    case Cons(x,xs) => if (n>x) Cons(x,smaller(n,xs)) else smaller(n,xs)
+  }
+
+  def equals(n:Int,list:List) : List = list match {
+    case Nil() => Nil()
+    case Cons(x,xs) => if (n==x) Cons(x,equals(n,xs)) else equals(n,xs)
+  }
+
+  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))
+
+  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(quickSort(ls))
+  }
+}

pldi2011-testcases/RedBlackTree.scala

+import scala.collection.immutable.Set
+//import scala.collection.immutable.Multiset
+
+object RedBlackTree { 
+  sealed abstract class Color
+  case class Red() extends Color
+  case class Black() extends Color
+ 
+  sealed abstract class Tree
+  case class Empty() extends Tree
+  case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+  def content(t : Tree) : Set[Int] = t match {
+    case Empty() => Set.empty
+    case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
+  }
+
+  def size(t : Tree) : Int = t match {
+    case Empty() => 0
+    case Node(_, l, v, r) => size(l) + 1 + size(r)
+  }
+
+  def ins(x : Int, t: Tree): Tree = (t match {
+    case Empty() => Node(Red(),Empty(),x,Empty())
+    case Node(c,a,y,b) =>
+      if      (x < y)  balance(c, ins(x, a), y, b)
+      else if (x == y) Node(c,a,y,b)
+      else             balance(c,a,y,ins(x, b))
+  }) ensuring (res => (
+             content(res) == content(t) ++ Set(x) 
+//          && size(t) <= size(res) && size(res) < size(t) + 2)
+              ))
+
+  def add(x: Int, t: Tree): Tree = {
+    makeBlack(ins(x, t))
+  } ensuring (content(_) == content(t) ++ Set(x))
+  
+  def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = (Node(c,a,x,b) match {
+    case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) => 
+      Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+    case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) => 
+      Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+    case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) => 
+      Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+    case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) => 
+      Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+    case Node(c,a,xV,b) => Node(c,a,xV,b)
+  }) ensuring (res => content(res) == content(Node(c,a,x,b)))
+
+  def makeBlack(n: Tree): Tree = n match {
+    case Node(Red(),l,v,r) => Node(Black(),l,v,r)
+    case _ => n
+  }
+}

pldi2011-testcases/TreeMap.scala

@@ -76,12 +76,18 @@ object TreeMap {
   }
 
   def create(k: Int, d: Int, l: TreeMap, r: TreeMap): TreeMap = {
-    require(nodeHeightsAreCorrect(l) && nodeHeightsAreCorrect(r) && isBalanced(l) && isBalanced(r) &&
-      height(l) - height(r) <= 2 && height(r) - height(l) <= 2)
+    require(
+      nodeHeightsAreCorrect(l) && nodeHeightsAreCorrect(r) && isBalanced(l) && isBalanced(r) &&
+      height(l) - height(r) <= 2 && height(r) - height(l) <= 2 &&
+      isBST(l) && isBST(r) // and max l < min r
+    )
     val hl = height(l)
     val hr = height(r)
     Node(k, d, l, r, mmax(hl, hr) + 1)
-  } ensuring(res => setOf(res) == Set(k) ++ setOf(l) ++ setOf(r) && isBalanced(res))
+  } ensuring(
+    res => setOf(res) == Set(k) ++ setOf(l) ++ setOf(r) && 
+    isBalanced(res) && isBST(res)
+  )
 
   def balance(x: Int, d: Int, l: TreeMap, r: TreeMap): TreeMap = {
     require(
@@ -125,7 +131,7 @@ object TreeMap {
       }
     } else
       Node(x, d, l, r, if(hl >= hr) hl + 1 else hr + 1)
-  } ensuring(isBalanced(_))
+  } ensuring(res => isBalanced(res)) // && setOf(res) == Set[Int](x) ++ setOf(l) ++ setOf(r))
 
   def add(x: Int, data: Int, tm: TreeMap): TreeMap = {
     require(isBalanced(tm) && nodeHeightsAreCorrect(tm))
@@ -139,9 +145,9 @@ object TreeMap {
         else
           balance(v, d, l, add(x, data, r))
     }
-  } ensuring(isBalanced(_))
+  } ensuring(res => isBalanced(res)) // && setOf(res) == Set(x) ++ setOf(tm))
 
-  def removeMinBinding(t: TreeMap): Triple = {
+  def removeMinBinding(t: TreeMap): Tuple = {
     require(isBalanced(t) && (t match {
       case Empty() => false
       case _ => true
@@ -151,11 +157,15 @@ object TreeMap {
         l match {
           case Empty() => Triple(x, d, r)
           case Node(_,_,ll, lr, h2) =>
-            val triple = removeMinBinding(l)
-            Triple(triple.key, triple.datum, balance(x, d, triple.tree, r))
+            removeMinBinding(l) match {
+              case Triple(key, datum, tree) =>
+                Triple(key, datum, balance(x, d, tree, r))
+            }
         }
     }
-  } ensuring(res => isBalanced(res.tree))
+  } ensuring(res => res match {
+    case Triple(resKey, _, resTree) => isBalanced(resTree) // && (setOf(resTree) == setOf(t) -- Set(resKey)) && setOf(resTree) ++ Set(resKey) == setOf(t)
+  })
 
   // m is not used here!
   def merge(m: Int, t1: TreeMap, t2: TreeMap): TreeMap = {
@@ -166,11 +176,12 @@ object TreeMap {
         t2 match {
           case Empty() => t1
           case Node(r, _, rl, rr, h2) =>
-            val triple = removeMinBinding(t2)
-            balance(triple.key, triple.datum, t1, triple.tree)
+            removeMinBinding(t2) match {
+              case Triple(key, datum, tree) => balance(key, datum, t1, tree)
+            }
         }
     }
-  } ensuring(isBalanced(_))
+  } ensuring(res => isBalanced(res)) // && setOf(res) == setOf(t1) ++ setOf(t2))
 
   def remove(x: Int, t: TreeMap): TreeMap = {
     require(isBalanced(t))
@@ -184,7 +195,7 @@ object TreeMap {
         else
           balance(v, d, l, remove(x, r))
     }
-  } ensuring(isBalanced(_))
+  } ensuring(res => isBalanced(res)) // && (setOf(res) == setOf(t) -- Set(x)))
 
   def find(t: TreeMap, x: Int): Int = {
     require(t match {
@@ -216,10 +227,10 @@ object TreeMap {
       v < k && iter2(l, v) && iter2(r, v)
   }
 
-  def checkBST(t: TreeMap): Boolean = t match {
+  def isBST(t: TreeMap): Boolean = t match {
     case Empty() => true
     case Node(v, _, l, r, _) =>
-      iter1(l, v) && iter2(r, v) && checkBST(l) && checkBST(r)
+      iter1(l, v) && iter2(r, v) && isBST(l) && isBST(r)
   }
 
   // We have a variant of AVL trees where the heights of the subtrees differ at