From 2bb9282dadfcbeeaee205a807cf23698181ebfb5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com>
Date: Sun, 14 Nov 2010 18:38:16 +0000
Subject: [PATCH] Copying sorting and RB tree examples from testcases
---
pldi2011-testcases/InsertionSort.scala | 98 ++++++++++++++++++++++++++
pldi2011-testcases/MergeSort.scala | 66 +++++++++++++++++
pldi2011-testcases/QuickSort.scala | 58 +++++++++++++++
pldi2011-testcases/RedBlackTree.scala | 54 ++++++++++++++
pldi2011-testcases/TreeMap.scala | 41 +++++++----
5 files changed, 302 insertions(+), 15 deletions(-)
create mode 100644 pldi2011-testcases/InsertionSort.scala
create mode 100644 pldi2011-testcases/MergeSort.scala
create mode 100644 pldi2011-testcases/QuickSort.scala
create mode 100644 pldi2011-testcases/RedBlackTree.scala
diff --git a/pldi2011-testcases/InsertionSort.scala b/pldi2011-testcases/InsertionSort.scala
new file mode 100644
index 000000000..0db222160
--- /dev/null
+++ b/pldi2011-testcases/InsertionSort.scala
@@ -0,0 +1,98 @@
+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))
+ }
+}
diff --git a/pldi2011-testcases/MergeSort.scala b/pldi2011-testcases/MergeSort.scala
new file mode 100644
index 000000000..da575c8bb
--- /dev/null
+++ b/pldi2011-testcases/MergeSort.scala
@@ -0,0 +1,66 @@
+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))
+ }
+}
diff --git a/pldi2011-testcases/QuickSort.scala b/pldi2011-testcases/QuickSort.scala
new file mode 100644
index 000000000..83dd2c364
--- /dev/null
+++ b/pldi2011-testcases/QuickSort.scala
@@ -0,0 +1,58 @@
+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))
+ }
+}
diff --git a/pldi2011-testcases/RedBlackTree.scala b/pldi2011-testcases/RedBlackTree.scala
new file mode 100644
index 000000000..04ccb08fa
--- /dev/null
+++ b/pldi2011-testcases/RedBlackTree.scala
@@ -0,0 +1,54 @@
+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
+ }
+}
diff --git a/pldi2011-testcases/TreeMap.scala b/pldi2011-testcases/TreeMap.scala
index 5b734cf92..821458aa0 100644
--- a/pldi2011-testcases/TreeMap.scala
+++ b/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
--
GitLab