From 2a598b2035badcfde878a17682f1fc446c8882cc Mon Sep 17 00:00:00 2001
From: Tihomir Gvero <tihomir.gvero@gmail.com>
Date: Fri, 6 Nov 2009 20:28:58 +0000
Subject: [PATCH] Committing functional data structure examples for Udita.
---
tests/udita/BinarySearchTreeTest.scala | 85 ++++++++++
tests/udita/BinomialHeapTest.scala | 143 +++++++++++++++++
tests/udita/LeftistHeapTest.scala | 101 ++++++++++++
tests/udita/RedBlackTreeTest.scala | 135 ++++++++++++++++
.../SkewBinaryRandomAccessListTest.scala | 136 ++++++++++++++++
tests/udita/SplayHeapTest.scala | 148 ++++++++++++++++++
6 files changed, 748 insertions(+)
create mode 100644 tests/udita/BinarySearchTreeTest.scala
create mode 100644 tests/udita/BinomialHeapTest.scala
create mode 100644 tests/udita/LeftistHeapTest.scala
create mode 100644 tests/udita/RedBlackTreeTest.scala
create mode 100644 tests/udita/SkewBinaryRandomAccessListTest.scala
create mode 100644 tests/udita/SplayHeapTest.scala
diff --git a/tests/udita/BinarySearchTreeTest.scala b/tests/udita/BinarySearchTreeTest.scala
new file mode 100644
index 000000000..a4d63288e
--- /dev/null
+++ b/tests/udita/BinarySearchTreeTest.scala
@@ -0,0 +1,85 @@
+package udita
+
+import gov.nasa.jpf.jvm.Verify;
+
+object BinarySearchTreeTest extends Application {
+
+ sealed abstract class BinarySearchTree;
+ case object Empty extends BinarySearchTree;
+ case class Node(left: BinarySearchTree, value:Int, right:BinarySearchTree) extends BinarySearchTree;
+
+ def size(t: BinarySearchTree): Int = t match {
+ case Empty => 0;
+ case Node(left,value,right) => size(left) + 1 + size(right);
+ }
+
+ def add(x: Int, t:BinarySearchTree):BinarySearchTree =t match {
+ case Empty => Node(Empty,x,Empty);
+ case Node(left,value,right) if (x < value) => Node(add(x,left),value,right);
+ case Node(left,value,right) if (x >= value) => Node(left,value,add(x,right));
+ }
+
+ def contains(x :Int, t:BinarySearchTree):Boolean = t match {
+ case Empty => false;
+ case Node(left,value,right) if (x == value) => true;
+ case Node(left,value,right) if (x < value) => contains(x,left);
+ case Node(left,value,right) if (x > value) => contains(x,right);
+ }
+
+ private def generateBinarySearchTree(treeSize:Int): BinarySearchTree = {
+ val size = Verify.getInt(1, treeSize);
+ val maxNodeValue = size - 1;
+ val t = getSubTree(size, 0, maxNodeValue);
+ System.out.println(t);
+ return t;
+ }
+
+ private def getSubTree(size:Int, min:Int, max:Int): BinarySearchTree = {
+ if (size == 0) return Empty;
+ if (size == 1) return Node(Empty, Verify.getInt(min,max), Empty);
+
+ val value = Verify.getInt(min,max);
+
+ val leftSize = value - min;
+ val rightSize = size - 1 - leftSize;
+
+ return Node(getSubTree(leftSize, min, value - 1), value, getSubTree(rightSize, value + 1, max));
+ }
+
+ def content(t:BinarySearchTree):Set[Int] = t match {
+ case Empty => Set.empty;
+ case Node(left,value,right) => (content(left) ++ Set(value) ++ content(right));
+ }
+
+// def forallTree(treeSize:Int,property : (BinarySearchTree => Boolean)):Boolean = {
+// property(generateBinarySearchTree(treeSize));
+// }
+//
+// def forallInt(min:Int, max:Int, property: (Int => Boolean)) : Boolean ={
+// property(Verify.getInt(min,max));
+// }
+
+ //val t = add(17, add(6, add(3, add(5,add(3,Empty)))));
+
+ //testing tree
+// System.out.println(t);
+// System.out.println(content(t));
+// System.out.println(size(t));
+// System.out.println(contains(5,t));
+
+ //testing getInt
+ //assert(forallInt(0,4,(x => forallTree(4,t => content(add(x,t)) == content(t) + x))));
+
+ def forAll(property:(BinarySearchTree,Int)=> Boolean){
+ assert(property(generateBinarySearchTree(4),Verify.getInt(0,4)));
+ }
+
+ forAll((t:BinarySearchTree, x:Int) => content(add(x,t)) == content(t) + x);
+
+ //System.out.println(generateBinarySearchTree(4));
+ //System.out.println("property: "+forallInt(0,4,(x => forallTree(4,t => content(add(x,t)) == content(t) + x))));
+}
+
+
+
+
diff --git a/tests/udita/BinomialHeapTest.scala b/tests/udita/BinomialHeapTest.scala
new file mode 100644
index 000000000..0099f703a
--- /dev/null
+++ b/tests/udita/BinomialHeapTest.scala
@@ -0,0 +1,143 @@
+package udita
+
+import scala.collection.immutable.Multiset;
+import gov.nasa.jpf.jvm.Verify;
+
+object BinomialHeapTest extends Application {
+ sealed case class BinomialHeap(trees:List[BinomialTree]);
+
+ sealed case class BinomialTree(rank:Int, value:Int, children:List[BinomialTree]);
+
+ def rankk(t1:BinomialTree):Int = t1 match {
+ case BinomialTree(rank, _, _) => rank;
+ }
+
+ def root(t1:BinomialTree):Int = t1 match {
+ case BinomialTree(_, value, _) => value;
+ }
+
+ def link(t1:BinomialTree, t2:BinomialTree):BinomialTree = t1 match {
+ case BinomialTree(rank1,value1,children1) => t2 match {
+ case BinomialTree(rank2,value2,children2) => {
+ if (value1 <= value2) BinomialTree(rank1+1, value1, t2::children1);
+ else BinomialTree(rank2+1, value2, t1::children2);
+ }
+ }
+ }
+
+ def insertTree(t:BinomialTree, trees:List[BinomialTree]):List[BinomialTree] = trees match {
+ case Nil => List(t);
+ case t1::ts1 => {
+ if (rankk(t) < rankk(t1)) t::trees; //bug t::ts1;
+ else insertTree(link(t,t1),ts1);
+ }
+ }
+
+ def insert(x:Int, trees:List[BinomialTree]):List[BinomialTree] = insertTree(BinomialTree(0,x,Nil), trees);
+
+ def insert(x:Int, heap:BinomialHeap):BinomialHeap = heap match {
+ case BinomialHeap(ts) => BinomialHeap(insert(x,ts));
+ }
+
+ def merge(ts1:List[BinomialTree],ts2:List[BinomialTree]):List[BinomialTree] = ts1 match {
+ case Nil => ts2;
+ case t1::tss1 => ts2 match {
+ case Nil => ts1;
+ case t2::tss2 => {
+ if (rankk(t1) < rankk(t2)) t1::merge(tss1,ts2);
+ else if (rankk(t2) < rankk(t1)) t2::merge(ts1,tss2);
+ else insertTree(link(t1,t2),merge(tss1,tss2));
+ }
+ }
+ }
+
+ def removeMinTree(ts:List[BinomialTree]):(BinomialTree,List[BinomialTree]) = ts match {
+ case t1::Nil => (t1,Nil);
+ case t1::ts1 => {
+ val (t11,ts11) = removeMinTree(ts1);
+ if (root(t1) <= root(t11)) (t1,ts1);
+ else (t11,t1::ts11);
+ }
+ case Nil => error("removing from empt tree");
+ }
+
+ def findMin(ts:List[BinomialTree]):Int = {
+ val (t1,_) = removeMinTree(ts);
+ root(t1);
+ }
+
+ def deleteMin(ts:List[BinomialTree]):List[BinomialTree] ={
+ val (BinomialTree(_,x,ts1),ts2) = removeMinTree(ts);
+ merge(ts1.reverse,ts2);
+ }
+
+ def deleteMin(heap:BinomialHeap):BinomialHeap = heap match {
+ case BinomialHeap(ts) => BinomialHeap(deleteMin(ts));
+ }
+
+ def findMin(heap:BinomialHeap):Int = heap match {
+ case BinomialHeap(ts) => findMin(ts);
+ }
+
+ def generateBinomialTree(rank:Int, min:Int, max:Int): BinomialTree = {
+ if(rank == 0) BinomialTree(rank, Verify.getInt(min,max), Nil);
+ else {
+ val value = Verify.getInt(min,max - rank);
+ var list = List[BinomialTree]();
+ for(i <- 0 until rank) {
+ list = generateBinomialTree(i,value+1,max)::list;
+ }
+ BinomialTree(rank,value,list);
+ }
+ }
+
+ def generateBinomialHeap(heapSize:Int):BinomialHeap = {
+ var div:Int = heapSize;
+ var list = List[BinomialTree]();
+ var i = 0;
+ while(div > 0) {
+ var mod:Int = div % 2;
+ if (mod == 1) {
+ list= list ::: List(generateBinomialTree(i,0,heapSize));
+ }
+ div = div/2;
+ i+=1;
+ }
+ BinomialHeap(list);
+ }
+
+ def content(t : BinomialHeap): Multiset[Int] = {
+ def inner(t: BinomialTree, mset: Multiset[Int]): Multiset[Int] = t match {
+ case BinomialTree(rank, value, children) => {
+ innerList(children, mset +++ List(value));
+ }
+ }
+ def innerList(ts: List[BinomialTree], mset:Multiset[Int]): Multiset[Int] = ts match {
+ case Nil => mset
+ case t::tss => inner(t, innerList(tss,mset))
+ }
+ t match {
+ case BinomialHeap(ts) => innerList(ts,Multiset.empty[Int]);
+ }
+ }
+
+
+ var heap = BinomialHeap(Nil);
+ heap = insert(5,insert(26,insert(1,insert(17,insert(4,heap)))));
+
+// System.out.println(heap);
+// System.out.println(findMin(heap));
+// System.out.println(deleteMin(heap));
+// System.out.println(content(heap));
+//
+// System.out.println(content(insert(1,heap)) == content(heap) +++ List(1));
+// System.out.println(generateBinomialHeap(3));
+//
+
+ def forAll(property : ((BinomialHeap,Int) => Boolean)){
+ assert(property(generateBinomialHeap(4), Verify.getInt(0,4)));
+ }
+
+ forAll((heap, value) => (content(insert(value,heap)) == content(heap) +++ List(value)));
+
+}
diff --git a/tests/udita/LeftistHeapTest.scala b/tests/udita/LeftistHeapTest.scala
new file mode 100644
index 000000000..8e88501df
--- /dev/null
+++ b/tests/udita/LeftistHeapTest.scala
@@ -0,0 +1,101 @@
+package udita
+
+
+import scala.collection.immutable.Multiset;
+import gov.nasa.jpf.jvm.Verify;
+
+object LeftistHeapTest extends Application {
+
+ sealed abstract class Heap{
+ def rankk():Int = this match {
+ case Empty => 0;
+ case Node(rank,_,_,_) => rank;
+ }
+
+ def insert(x: Int): Heap = {
+ LeftistHeapTest.merge(this, Node(1,x,Empty,Empty))
+ }
+
+ def findMin(): Int = this match {
+ case Empty => Predef.error(toString());
+ case Node(_,x,_,_) => x
+ }
+
+// override def toString(): String = this match {
+// case Empty => "Empty";
+// case Node(rank,x,left,right) => "Node("+rank+","+x+","+left+","+right+")";
+// }
+
+ //ensuring(res => res == min(content(this).elements.toList))
+
+ def deleteMin(): Heap = this match {
+ case Empty => Predef.error(toString());
+ case Node(_, _, left: Heap, right: Heap) => LeftistHeapTest.merge(left,right);
+ }
+ //ensuring(res => content(res).equals(content(this) - findMin))
+ }
+
+ case class Node(rank:Int, value:Int, left:Heap, right:Heap) extends Heap;
+ case object Empty extends Heap;
+
+ def merge(heap1:Heap, heap2:Heap): Heap = heap1 match {
+ case Empty => heap2;
+ case Node(_, value1, left1, right1) => heap2 match {
+ case Empty => heap1;
+ case Node(_, value2, left2, right2) if (value1 <= value2) =>
+ makeAndSwap(left1, value1, merge(right1,heap2));
+ case Node(_, value2, left2, right2) if (value1 > value2) =>
+ makeAndSwap(left2, value2, merge(heap1,right2));
+ }
+ }
+
+ def makeAndSwap(left:Heap, value:Int, right:Heap): Heap = {
+ if(left.rankk() >= right.rankk()){
+ Node(right.rankk() + 1, value, left, right);
+ } else {
+ Node(left.rankk() + 1, value, right, left);
+ }
+ }
+
+
+ def forAllLeftistHeap(size:Int, property:(Heap=>Boolean)): Boolean = {
+ property(generateLeftistHeap(size));
+ }
+
+ def generateLeftistHeap(treeSize:Int):Heap = {
+ val size = Verify.getInt(1, treeSize);
+ val maxNodeValue = size - 1;
+ val t = getSubTree(size, -1, maxNodeValue - 1);
+ System.out.println(t);
+ return t;
+ }
+
+ private def getSubTree(size:Int, min:Int, max:Int): Heap = {
+ if (size == 0) return Empty;
+ if (size == 1) return Node(1, Verify.getInt(min+1,max+1), Empty, Empty);
+
+ val value = Verify.getInt(min+1,max+1);
+ val rightSize = Verify.getInt(0,(size - 1)/2);
+ val leftSize = size - 1 - rightSize;
+
+ val rightSub = getSubTree(rightSize, value, max);
+ val leftSub = getSubTree(leftSize, value, max);
+
+ return Node(rightSub.rankk() + 1, value, leftSub, rightSub);
+ }
+
+ def content(t : Heap): Multiset[Int] = {
+ def inner(t: Heap, mset: Multiset[Int]): Multiset[Int] = t match {
+ case Empty => mset
+ case Node(rank,value,left,right) => inner(right, inner(left, mset +++ List(value)))
+ }
+ inner(t,Multiset.empty[Int]);
+ }
+
+ def forAll(property : ((Heap,Int) => Boolean)){
+ assert(property(generateLeftistHeap(4), 0));//Verify.getInt(0,4)));
+ }
+
+ forAll((heap: Heap, value: Int) => content(heap.insert(value)) == content(heap) +++ List(value));
+
+}
\ No newline at end of file
diff --git a/tests/udita/RedBlackTreeTest.scala b/tests/udita/RedBlackTreeTest.scala
new file mode 100644
index 000000000..53c64e9e0
--- /dev/null
+++ b/tests/udita/RedBlackTreeTest.scala
@@ -0,0 +1,135 @@
+package udita
+
+import gov.nasa.jpf.jvm.Verify;
+
+object RedBlackTreeTest extends Application {
+
+ val RED:Boolean = true;
+ val BLACK:Boolean = false;
+
+ sealed abstract class Tree
+ case class Empty() extends Tree
+ case class Node(color: Boolean, left: Tree, value: Int, right: Tree) extends Tree
+
+
+ def member(x: Int, t:Tree): Boolean = t match {
+ case Empty() => false
+ case Node(_,a,y,b) =>
+ if (x < y) member(x,a)
+ else if (x > y) member(x,b)
+ else true
+ }
+
+ def insert(x: Int, t: Tree): Tree = {
+ def ins(t: Tree): Tree = t match {
+ case Empty() => Node(RED,Empty(),x,Empty())
+ case Node(c,a,y,b) =>
+ if (x < y) balance(c, ins(a), y, b)
+ else if (x == y) Node(c,a,y,b)
+ else balance(c,a,y,ins(b))
+ }
+ makeBlack(ins(t))
+ }
+
+ def balance(c: Boolean, a: Tree, x: Int, b: Tree): Tree = (c,a,x,b) match {
+ case (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 (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 (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 (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 (c,a,xV,b) => Node(c,a,xV,b)
+ }
+
+ /** makeBLACK: Turn a node BLACK. */
+ def makeBlack(n: Tree): Tree = n match {
+ case Node(RED,l,v,r) => Node(BLACK,l,v,r)
+ case _ => n
+ }
+
+ /* global invariants:
+ * RED-BLACK trees are binary search trees obeying two key invariants:
+ *
+ * (1) Any path from a root node to a leaf node contains the same number
+ * of BLACK nodes. (A balancing condition.)
+ *
+ * (2) RED nodes always have BLACK children.
+ *
+ */
+
+ /* Empty tree are consideRED to be BLACK */
+ def isBLACK(t: Tree): Boolean = t match {
+ case Node(RED,_,_,_) => false
+ case _ => true
+ }
+
+
+ def anyPathsContainsSameNumberOfBlackNodes(t: Tree): Boolean = {
+ def blacks(t: Tree, acc: Int): List[Int] = t match {
+ case Empty() => List(acc + 1) // because Empty are assumed to be BLACK
+ case Node(_,l,_,r) =>
+ val upAcc = if(isBLACK(t)) acc + 1 else acc
+ blacks(l,upAcc) ::: blacks(r,upAcc)
+ }
+ val paths = blacks(t, 0)
+
+ if(paths.isEmpty)
+ true
+ else
+ paths.forall(_ == paths.head)
+ }
+
+ def areRedNodeChildrenBlack(t: Tree): Boolean = t match {
+ case Node(RED,l,_,r) =>
+ isBLACK(l) && isBLACK(r) &&
+ areRedNodeChildrenBlack(l) && areRedNodeChildrenBlack(r)
+ case Node(BLACK,l,_,r) =>
+ areRedNodeChildrenBlack(l) && areRedNodeChildrenBlack(r)
+ case _ => true
+ }
+
+ def generateRedBlackTree(treeSize:Int): Tree = {
+ val t = generateBinarySearchTree(treeSize);
+ Verify.ignoreIf(!anyPathsContainsSameNumberOfBlackNodes(t) || !areRedNodeChildrenBlack(t));
+ return t;
+ }
+
+ private def generateBinarySearchTree(treeSize:Int): Tree = {
+ val size = Verify.getInt(1, treeSize);
+ val maxNodeValue = size - 1;
+ val t = getSubTree(size, 0, maxNodeValue);
+ return t;
+ }
+
+ private def getSubTree(size:Int, min:Int, max:Int): Tree = {
+ if (size == 0) return Empty();
+ if (size == 1) return Node(Verify.getBoolean(), Empty(), Verify.getInt(min,max), Empty());
+
+ val value = Verify.getInt(min,max);
+
+ val leftSize = value - min;
+ val rightSize = size - 1 - leftSize;
+
+ return Node(Verify.getBoolean(), getSubTree(leftSize, min, value - 1), value, getSubTree(rightSize, value + 1, max));
+ }
+
+ def content(t:Tree):Set[Int] = t match {
+ case Empty() => Set.empty;
+ case Node(_,left,value,right) => (content(left) ++ Set(value) ++ content(right));
+ }
+
+ def forAll(property: (Tree,Int) => Boolean){
+ val t = generateRedBlackTree(4);
+ val x = Verify.getInt(0,4);
+ assert(property(t,x));
+ System.out.println(x+" "+t);
+ }
+
+ forAll((t:Tree, x:Int) => ({val t1 = insert(x,t); anyPathsContainsSameNumberOfBlackNodes(t1) && areRedNodeChildrenBlack(t1)}));
+ //forAll{t: Tree => areRedNodeChildrenBlack(t)} //(2)
+
+ //generateRedBlackTree(4);
+
+}
diff --git a/tests/udita/SkewBinaryRandomAccessListTest.scala b/tests/udita/SkewBinaryRandomAccessListTest.scala
new file mode 100644
index 000000000..4f2ff61d2
--- /dev/null
+++ b/tests/udita/SkewBinaryRandomAccessListTest.scala
@@ -0,0 +1,136 @@
+package udita
+
+import scala.collection.immutable.Multiset;
+import gov.nasa.jpf.jvm.Verify;
+
+object SkewBinaryRandomAccessListTest extends Application {
+
+ sealed abstract class Tree
+ case class Leaf(w: Int) extends Tree
+ case class Node(w: Int, left: Tree, right: Tree) extends Tree
+
+ type RList = List[(Int, Tree)]
+
+ val empty = Nil
+
+ def isEmpty(ts: RList) = ts.isEmpty
+
+ def cons(w: Int, ts: RList): RList = ts match {
+ case (w1,t1) :: (w2,t2) :: rest if (w1 == w2) =>
+ (1+w1+w2, Node(w,t1,t2)) :: rest
+
+ case _ =>
+ (1, Leaf(w)) :: ts
+ }
+
+ def head(ts: RList): Int = ts match {
+ case Nil => error("head of empty list")
+ case (1, Leaf(x)) :: ts => x
+ case (_, Node(x, _, _)) :: ts => x
+ }
+
+ def tail(ts: RList): RList = ts match {
+ case Nil => error("tail of empty list")
+ case (1, Leaf(x)) :: ts => ts
+ case (w, Node(x, t1, t2)) :: rest =>
+ (w/2, t1) :: (w/2, t2) :: rest
+ }
+
+ def lookup(i: Int, ts: RList): Int = ts match {
+ case Nil => error("lookup of empty list")
+ case (w,t) :: ts =>
+ if (i < w) lookupTree(w,i,t)
+ else lookup(i-w, ts)
+ }
+
+ def lookupTree(w: Int, i: Int, t: Tree): Int = (w,i,t) match {
+ case (1,0, Leaf(x)) => x
+ case tuple @ (1,_,Leaf(x)) => error("lookupTree: error for "+tuple)
+ case (_,0, Node(x,_,_)) => x
+ case (_,_,Node(x,t1,t2)) =>
+ if (i < w/2) lookupTree(w/2,i-1,t1)
+ else lookupTree(w/2,i-1-w/2,t2)
+ }
+
+ def updateTree(w: Int, i: Int, y: Int, t: Tree): Tree = (w,i,y,t) match {
+ case (1,0,_,Leaf(x)) => Leaf(y)
+ case tuple @ (1,_,_,Leaf(x)) => error("updateTree: Error for "+tuple)
+ case (_,0,_,Node(x,t1,t2)) => Node(y,t1,t2)
+ case (_,_,_,Node(x,t1,t2)) =>
+ if (i <= w/2) Node(x,updateTree(w/2,i-1,y,t1),t2)
+ else Node(x,t1, updateTree(w/2,i-1-w/2,y,t2))
+ }
+
+
+ def update(i: Int, y: Int, ts: RList): RList = ts match {
+ case Nil => error("update of empty list")
+ case (w,t) :: ts =>
+ if (i < w) (w, updateTree(w,i,y,t)) :: ts
+ else (w,t) :: update(i-w,y,ts)
+ }
+
+ def incTreeList(ws:List[Int]):List[Int] = ws match {
+ case w1::w2::rest => {
+ if (w1 == w2) (1+w1+w2)::rest;
+ else 1 :: ws;
+ }
+ case _ => 1 :: ws;
+ }
+
+ def makeSizeList(size:Int):List[Int] = {
+ var list:List[Int] = Nil;
+ for(i <- 0 until size) {
+ list = incTreeList(list);
+ }
+ return list;
+ }
+
+ def generateSkewBinaryList(maxSize:Int): RList = {
+ val size = Verify.getInt(1, maxSize);
+ val sizeList = makeSizeList(size);
+ val rl = generateAllTrees(sizeList);
+ System.out.println(rl);
+ return rl;
+ }
+
+ def generateAllTrees(sizeList:List[Int]):RList = sizeList match {
+ case hd::rest => List((hd, generateTree(hd))):::generateAllTrees(rest);
+ case Nil => Nil;
+ }
+
+ private def generateTree(size:Int): Tree = {
+ val maxNodeValue = size - 1;
+ val t = getSubTree(size, 0, 0);//should go up to maxNodeValue
+ //System.out.println(t);
+ return t;
+ }
+
+ private def getSubTree(size:Int, min:Int, max:Int): Tree = {
+ if (size == 1) return Leaf(Verify.getInt(min,max));
+ val value = Verify.getInt(min,max);
+ val subtreeSize = (size-1) / 2;
+ return Node(value, getSubTree(subtreeSize, min, max), getSubTree(subtreeSize, min, max));
+ }
+
+ def content(t : RList): Multiset[Int] = {
+ def inner(t: Tree, mset: Multiset[Int]): Multiset[Int] = t match {
+ case Leaf(value) => mset +++ List(value);
+ case Node(value, left, right) => inner(right,inner(left, mset +++ List(value)));
+ }
+ def innerList(ts: RList, mset:Multiset[Int]): Multiset[Int] = ts match {
+ case Nil => mset
+ case (w,t)::tss => inner(t, innerList(tss,mset))
+ }
+ innerList(t,Multiset.empty[Int]);
+ }
+
+
+ //generateSkewBinaryList(4);
+
+ def forAll(property : ((RList,Int) => Boolean)){
+ assert(property(generateSkewBinaryList(4), 4));//Verify.getInt(0,4)));
+ }
+
+ forAll((skew, value) => (content(cons(value,skew)) == content(skew) +++ List(value)));
+
+}
diff --git a/tests/udita/SplayHeapTest.scala b/tests/udita/SplayHeapTest.scala
new file mode 100644
index 000000000..ea31f659d
--- /dev/null
+++ b/tests/udita/SplayHeapTest.scala
@@ -0,0 +1,148 @@
+package udita
+
+import gov.nasa.jpf.jvm.Verify;
+
+object SplayHeapTest extends Application {
+ sealed abstract class Heap
+ case class E() extends Heap
+ case class T(x: Int, a: Heap, b: Heap) extends Heap
+
+ def isEmpty(h: Heap): Boolean = h.isInstanceOf[E]
+
+ def partition(pivot: Int, t: Heap): (Heap,Heap) = t match {
+ case E() => (E(),E())
+ case T(x,a,b) =>
+ if(x <= pivot) b match {
+ case E() => (T(x,a,E()),E())
+ case T(y,b1,b2) =>
+ if(y <= pivot) {
+ val (small,big) = partition(pivot,b2)
+ val r1 = T(y,T(x,a,b1),small)
+ val r2 = big
+ (r1,r2)
+ } else {
+ val (small,big) = partition(pivot,b1)
+ val r1 = T(x, a, small)
+ val r2 = T(y, big, b2)
+ (r1,r2)
+ }
+ } else a match {
+ case E() => (E(), T(x,E(),b))
+ case T(y,a1,a2) =>
+ if(y <= pivot) {
+ val (small,big) = partition(pivot,a2)
+ val r1 = T(y,a1,small)
+ val r2 = T(x,big,b)
+ (r1,r2)
+ } else {
+ val (small,big) = partition(pivot,a1)
+ val r1 = small
+ val r2 = T(y,big,T(x,a2,b))
+ (r1,r2)
+ }
+ }
+ }
+
+ def insert(x: Int, t: Heap): Heap = {
+ val (a,b) = partition(x,t)
+ T(x,a,b)
+ }
+
+ def merge(t1: Heap, t2: Heap): Heap = t1 match {
+ case E() => t2
+ case T(x,a,b) =>
+ val (ta,tb) = partition(x,t2)
+ val a1 = merge(ta,a)
+ val b1 = merge(tb,b)
+ T(x,a1,b1)
+ }
+
+ def deleteMin(t: Heap): Heap = t match {
+ case E() => error("empty")
+ case T(x,E(),b) => b
+ case T(y,T(x,E(),b),c) => T(y,b,c)
+ case T(y,T(x,a,b),c) => T(x,deleteMin(a),T(y,b,c))
+ }
+
+ def deleteMin2(t: Heap): (Int,Heap) = t match {
+ case E() => error("empty")
+ case T(x,E(),b) => (x, b)
+ case T(y,T(x,E(),b),c) => (x,T(y,b,c))
+ case T(y,T(x,a,b),c) =>
+ val (r, a1) = deleteMin2(a)
+ (r,T(x,a1,T(y,b,c)))
+ }
+
+ def findMin(t: Heap): Int = t match {
+ case E() => error("empty")
+ case T(x,E(),b) => x
+ case T(x,a,b) => findMin(a)
+ }
+
+ def findMin2(t: Heap): (Int,Heap) = t match {
+ case E() => error("empty")
+ case T(x,E(),b) => (x, t)
+ case T(x,a,b) =>
+ val (x1, a1) = findMin2(a)
+ (x1,T(x,a1,b))
+ }
+
+ def app(x: Int, ys: List[Int], zs: List[Int]): List[Int] = ys match {
+ case Nil => x :: zs
+ case y :: ys => y :: app(x,ys,zs)
+ }
+
+
+ def to_list(t: Heap): List[Int] = t match {
+ case E() => Nil
+ case T(x,a,b) => app(x,to_list(a),to_list(b))
+ }
+
+ def check_sorted(xs: List[Int]): Boolean = xs match {
+ case Nil => true
+ case x :: xs =>
+ xs.forall(x <= _) && check_sorted(xs)
+ }
+
+ def to_list2(t: Heap): List[Int] = {
+ val xs = to_list(t)
+ check_sorted(xs)
+ xs
+ }
+
+ def generateSplayHeap(treeSize:Int): Heap = {
+ return generateBinarySearchTree(treeSize);
+ }
+
+ private def generateBinarySearchTree(treeSize:Int): Heap = {
+ val size = Verify.getInt(1, treeSize);
+ val maxNodeValue = size - 1;
+ val t = getSubTree(size, 0, maxNodeValue);
+ return t;
+ }
+
+ private def getSubTree(size:Int, min:Int, max:Int): Heap = {
+ if (size == 0) return E();
+ if (size == 1) return T(Verify.getInt(min,max), E(), E());
+
+ val value = Verify.getInt(min,max);
+
+ val leftSize = value - min;
+ val rightSize = size - 1 - leftSize;
+
+ return T(value, getSubTree(leftSize, min, value - 1), getSubTree(rightSize, value + 1, max));
+ }
+
+ def content(t:Heap):Set[Int] = t match {
+ case E() => Set.empty;
+ case T(value,left,right) => (content(left) ++ Set(value) ++ content(right));
+ }
+
+ def forAll(property: (Heap) => Boolean){
+ val t = generateSplayHeap(4);
+ assert(property(t));
+ System.out.println(t);
+ }
+
+ forAll{h: Heap => check_sorted(to_list(h))}
+}
--
GitLab