mergesort example and updated 'forall' script.

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}

tests/plugin/kawaguchi/MergeSort.scala

+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]) = {}
+}