From 0ed920127a5bcee51167af7799bc09f20c59f2f1 Mon Sep 17 00:00:00 2001
From: Mirco Dotta <mirco.dotta@gmail.com>
Date: Thu, 9 Jul 2009 16:09:22 +0000
Subject: [PATCH] mergesort example and updated 'forall' script.
---
forall-tests.sh | 11 ++++++
tests/plugin/kawaguchi/MergeSort.scala | 47 ++++++++++++++++++++++++++
2 files changed, 58 insertions(+)
create mode 100644 tests/plugin/kawaguchi/MergeSort.scala
diff --git a/forall-tests.sh b/forall-tests.sh
index 81c2729f1..bcfcc1721 100755
--- a/forall-tests.sh
+++ b/forall-tests.sh
@@ -74,6 +74,9 @@ scalac plugin/PropositionalLogic.scala
scalac plugin/SetRedBlackTree.scala
scalac plugin/ConsSnoc.scala
+scalac plugin/kawaguchi/InsertSort.scala
+scalac plugin/kawaguchi/MergeSort.scala
+
cd ..
# Scala compiler with the Funcheck plugin integrated
@@ -100,6 +103,9 @@ export PropositionalLogic="plugin.PropositionalLogic"
export SetRedBlackTree="plugin.SetRedBlackTree"
export ConsSnoc="plugin.ConsSnoc"
+export InsertSort="plugin.kawaguchi.InsertSort"
+export MergeSort="plugin.kawaguchi.MergeSort"
+
echo " - Testing ${BST}"
scala ${BST}
@@ -121,3 +127,8 @@ scala ${PropositionalLogic}
echo " - Testing ${ConsSnoc}"
scala ${ConsSnoc}
+echo " - Testing ${InsertSort}"
+scala ${InsertSort}
+
+echo " - Testing ${MergeSort}"
+scala ${MergeSort}
diff --git a/tests/plugin/kawaguchi/MergeSort.scala b/tests/plugin/kawaguchi/MergeSort.scala
new file mode 100644
index 000000000..4c3f4b5d8
--- /dev/null
+++ b/tests/plugin/kawaguchi/MergeSort.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 MergeSort {
+
+ 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)
+ 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]) = {}
+}
--
GitLab