From 1308611ea92b41e90d12ca210e1538b6dee94b51 Mon Sep 17 00:00:00 2001
From: Mirco Dotta <mirco.dotta@gmail.com>
Date: Fri, 10 Jul 2009 11:06:59 +0000
Subject: [PATCH] Adding new examples from Online Demo for Data Structure
Verification (http://pho.ucsd.edu/liquid/)
---
tests/plugin/kawaguchi/MergeSortBug.scala | 47 ++++++
tests/plugin/kawaguchi/MiniBDD.scala | 177 ++++++++++++++++++++++
tests/plugin/kawaguchi/QuickSort.scala | 46 ++++++
3 files changed, 270 insertions(+)
create mode 100644 tests/plugin/kawaguchi/MergeSortBug.scala
create mode 100644 tests/plugin/kawaguchi/MiniBDD.scala
create mode 100644 tests/plugin/kawaguchi/QuickSort.scala
diff --git a/tests/plugin/kawaguchi/MergeSortBug.scala b/tests/plugin/kawaguchi/MergeSortBug.scala
new file mode 100644
index 000000000..bd2b245bf
--- /dev/null
+++ b/tests/plugin/kawaguchi/MergeSortBug.scala
@@ -0,0 +1,47 @@
+package plugin.kawaguchi
+
+import funcheck.lib.Specs._
+
+/* Example from paper "Type-based Data Structure Verification"
+ * http://pho.ucsd.edu/liquid/demo/index2.php */
+
+object MergeSortBug {
+
+ def halve(xs: List[Int]): (List[Int],List[Int]) = xs match {
+ case Nil => (Nil,Nil)
+ case x :: xs =>
+ val (ys,zs) = halve(xs)
+ (x :: zs, ys)
+ }
+
+ def merge(xs: List[Int], ys: List[Int]): List[Int] = (xs,ys) match {
+ case (Nil,_) => ys
+ case (_,Nil) => xs
+ case (x :: xs, y :: ys) =>
+ if (x < y) x :: merge(xs, y :: ys)
+ else y :: merge(x:: xs, ys)
+ }
+
+ def mergesort(ps: List[Int]): List[Int] = ps match {
+ case Nil => Nil
+ //case List(p) => List(p) XXX: BUG: Missing case
+ case _ =>
+ val (qs,rs) = halve(ps)
+ val qs1 = mergesort(qs)
+ val rs1 = mergesort(rs)
+ merge(qs1,rs1)
+ }
+
+ def check(xs: List[Int]): Boolean = xs match {
+ case x :: y :: xs =>
+ x <= y && check(y :: xs)
+
+ case _ => true
+ }
+
+ def test(xs: List[Int]): Boolean = check(mergesort(xs))
+
+ forAll{xs: List[Int] => test(xs)}
+
+ def main(args: Array[String]) = {}
+}
diff --git a/tests/plugin/kawaguchi/MiniBDD.scala b/tests/plugin/kawaguchi/MiniBDD.scala
new file mode 100644
index 000000000..0678bf4b2
--- /dev/null
+++ b/tests/plugin/kawaguchi/MiniBDD.scala
@@ -0,0 +1,177 @@
+package plugin.kawaguchi
+
+/* Example from paper "Type-based Data Structure Verification"
+ * http://pho.ucsd.edu/liquid/demo/index2.php */
+
+import funcheck.lib.Specs._
+
+object MiniBDD {
+
+ @generator
+ sealed abstract class BDD
+ case class Node(v: Int, low: BDD, high: BDD) extends BDD
+ case class Zero() extends BDD
+ case class One() extends BDD
+
+ @generator
+ sealed class Op
+ case class And() extends Op
+ case class Or() extends Op
+ case class Imp() extends Op
+ case class Any(f: (Boolean,Boolean) => Boolean) extends Op
+
+ def myfail: BDD = {
+ assert(false)
+ null
+ }
+
+ def bdd2int(b: BDD): Int = b match {
+ case Zero() | One() => 1000
+ case Node(v,_,_) => v
+ }
+
+ def utag(b: BDD): Int = b match {
+ case Zero() => 0
+ case One() => 1
+ case Node(v,_,_) => v
+ }
+
+ def low(b: BDD): BDD = b match {
+ case Node(_,l,_) => l
+ case _ => myfail
+ }
+
+ def high(b: BDD): BDD = b match {
+ case Node(_,_,h) => h
+ case _ => myfail
+ }
+
+
+ val zero = Zero()
+ val one = One()
+
+ def of_bool(b: Boolean): BDD = if(b) one else zero
+
+ def check(b: BDD): Boolean = b match {
+ case Zero() | One() => true
+ case Node(v,l,h) =>
+ (v < bdd2int(l)) &&
+ (v < bdd2int(h)) &&
+ check(l) && check(h)
+ }
+
+ def mk(x: Int, low: BDD, high: BDD) =
+ if(low == high) low else Node(x,low,high)
+
+ def empty = Map.empty[BDD,BDD]
+ def empty2 = Map.empty[(BDD,BDD),BDD]
+
+ def mk_not(x: BDD): BDD = {
+ val cache = empty
+ assert(check(x))
+
+ def mk_not_rec(cache: Map[BDD,BDD], x: BDD): (Map[BDD,BDD],BDD) = {
+ cache.get(x) match {
+ case Some(x) =>
+ (cache,x)
+ case None => {
+ val (table,res) = {
+ x match {
+ case Zero() => (cache,one)
+ case One() => (cache,zero)
+ case Node(v,l,h) =>
+ val (cachel,ll) = mk_not_rec(cache,l)
+ val (cacheh, hh) = mk_not_rec(cache,h)
+ (cachel ++ cacheh, mk(v,ll,hh))
+ }
+ }
+
+ (table + ((x -> res)),res)
+ }
+ }
+ }
+
+ val (_,rv) = mk_not_rec(cache, x)
+ assert(check(rv))
+ rv
+ }
+
+ def apply_op(op: Op, b1: Boolean, b2: Boolean): Boolean = op match {
+ case And() => b1 && b2
+ case Or() => b1 || b2
+ case Imp() => !b1 || b2
+ case Any(f) => f(b1,b2)
+ }
+
+ def gapply(op: Op): (BDD,BDD) => BDD = {
+ val op_z_z = of_bool(apply_op(op, false,false))
+ val op_z_o = of_bool(apply_op(op, false,true))
+ val op_o_z = of_bool(apply_op(op, true,false))
+ val op_o_o = of_bool(apply_op(op, true,true))
+
+ (b1: BDD, b2: BDD) => {
+ val cache = empty2
+
+ def app(cache: Map[(BDD,BDD),BDD], u1: BDD, u2: BDD): (Map[(BDD,BDD),BDD], BDD) = {
+ def default(res: BDD) = (cache,res)
+ op match {
+ case And() =>
+ if(u1 == u2) default(u1)
+ else if(u1 == zero || u2 == zero) default(zero)
+ else if(u1 == one) default(u2)
+ else if(u2 == one) default(u1)
+ else app_gen(cache, u1,u2)
+
+ case Or() =>
+ if(u1 == u2) default(u1)
+ else if(u1 == one || u2 == one) default(one)
+ else if(u1 == zero) default(u2)
+ else if(u2 == zero) default(u1)
+ else app_gen(cache, u1,u2)
+
+ case Imp() =>
+ if(u1 == zero) default(one)
+ else if(u1 == one) default(u2)
+ else if(u2 == one) default(u1)
+ else app_gen(cache, u1,u2)
+
+ case Any(_) => app_gen(cache, u1,u2)
+ }
+ }
+
+ def app_gen(cache: Map[(BDD,BDD),BDD], u1: BDD, u2: BDD): (Map[(BDD,BDD),BDD],BDD) = (u1,u2) match {
+ case (Zero(),Zero()) => (cache, op_z_z)
+ case (Zero(),One()) => (cache, op_z_o)
+ case (One(),Zero()) => (cache, op_o_z)
+ case (One(),One()) => (cache, op_o_o)
+ case _ =>
+ cache.get((u1,u2)) match {
+ case Some(x) => (cache, x)
+ case None =>
+ val (cacheres, res) = {
+ val v1 = bdd2int(u1)
+ val v2 = bdd2int(u2)
+ if(v1 == v2) {
+ val (cachelow,applow) = app(cache, low(u1),low(u2))
+ val (cachehigh,apphigh) = app(cache, high(u1),high(u2))
+ (cachelow ++ cachehigh, mk(v1, applow, apphigh))
+ } else if(v1 < v2) {
+ val (cachelow,applow) = app(cache, low(u1),u2)
+ val (cachehigh,apphigh) = app(cache, high(u1),u2)
+ (cachelow ++ cachehigh, mk(v1, applow, apphigh))
+ } else {
+ val (cachelow,applow) = app(cache, u1,low(u2))
+ val (cachehigh,apphigh) = app(cache, u1,high(u2))
+ (cachelow ++ cachehigh, mk(v2, applow, apphigh))
+ }
+ }
+ (cacheres + (((u1,u2) -> res)), res)
+ }
+ }
+
+ val (_,res) = app(cache, b1, b2)
+ res
+
+ }
+ }
+}
diff --git a/tests/plugin/kawaguchi/QuickSort.scala b/tests/plugin/kawaguchi/QuickSort.scala
new file mode 100644
index 000000000..34a7af897
--- /dev/null
+++ b/tests/plugin/kawaguchi/QuickSort.scala
@@ -0,0 +1,46 @@
+package plugin.kawaguchi
+
+/* Example from paper "Type-based Data Structure Verification"
+ * http://pho.ucsd.edu/liquid/demo/index2.php */
+
+import funcheck.lib.Specs._
+
+object QuickSort {
+
+ sealed abstract class Top(v: Int)
+ case class T(v: Int) extends Top(v)
+ case class F(v: Int) extends Top(v)
+
+ def partition(f: Int => Top, xs: List[Int]): (List[Int],List[Int]) = xs match {
+ case Nil => (Nil,Nil)
+ case x :: xs =>
+ val (ts,fs) = partition(f, xs)
+ f(x) match {
+ case T(x) => (x :: ts, fs)
+ case F(x) => (ts, x :: fs)
+ }
+ }
+
+
+ def quicksort(xs: List[Int]): List[Int] = xs match {
+ case Nil => Nil
+ case x :: xs =>
+ val (ls,rs) = partition(y => if (y < x) T(y) else F(x), xs)
+ val ls1 = quicksort(ls)
+ val rs1 = quicksort(rs)
+ (x :: ls1) ::: rs1
+ }
+
+ def check(xs: List[Int]): Boolean = xs match {
+ case Nil => true
+ case List(x) => true
+ case x :: y :: xs =>
+ (x <= y) && check(y :: xs)
+ }
+
+ def test(xs: List[Int]): Boolean = check(quicksort(xs))
+
+ forAll{xs: List[Int] => test(xs)}
+
+ def main(args: Array[String]) = {}
+}
--
GitLab