From 015ebd6bee1f8113caaa704367086b91d5b1f9cb Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <vkuncak@gmail.com>
Date: Fri, 10 Jul 2009 15:40:23 +0000
Subject: [PATCH] heap with positive elements
---
tests/plugin/kawaguchi/PosSplayHeap.scala | 143 ++++++++++++++++++++++
1 file changed, 143 insertions(+)
create mode 100644 tests/plugin/kawaguchi/PosSplayHeap.scala
diff --git a/tests/plugin/kawaguchi/PosSplayHeap.scala b/tests/plugin/kawaguchi/PosSplayHeap.scala
new file mode 100644
index 000000000..c97c2a20d
--- /dev/null
+++ b/tests/plugin/kawaguchi/PosSplayHeap.scala
@@ -0,0 +1,143 @@
+package plugin.kawaguchi
+
+/* Example from paper "Type-based Data Structure Verification"
+ * http://pho.ucsd.edu/liquid/demo/index2.php */
+
+/* Splay Heaps: Okasaki's "Purely Functional Data Structures" p.50 Fig. 5.5. */
+
+import funcheck.lib.Specs._
+
+object SplayHeap {
+
+
+ sealed abstract class Heap
+ @generator 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 require[T](property : Boolean, original : T)(code : => T) : T = {
+ if (property) {
+ code
+ } else {
+ original
+ }
+ }
+
+ case class IntPos(x : Int)
+
+ @generator
+ def mkIntPos(x : Int) = IntPos(abs(x))
+
+ @generator
+ def insert(x0: IntPos, t: Heap): Heap = {
+ val x = x0.x
+ 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] = {
+ // println(t)
+ 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
+ }
+
+ forAll{h: Heap => check_sorted(to_list(h))}
+
+ def main(args: Array[String]) = {}
+}
--
GitLab