From d995dd2d1b0c13ff90da801c18549848e5ef534f Mon Sep 17 00:00:00 2001
From: Mirco Dotta <mirco.dotta@gmail.com>
Date: Thu, 9 Jul 2009 15:47:07 +0000
Subject: [PATCH] Added example from paper Type-based Data Structure
Verification
---
tests/plugin/kawaguchi/InsertSort.scala | 39 +++++++++++++++++++++++++
1 file changed, 39 insertions(+)
create mode 100644 tests/plugin/kawaguchi/InsertSort.scala
diff --git a/tests/plugin/kawaguchi/InsertSort.scala b/tests/plugin/kawaguchi/InsertSort.scala
new file mode 100644
index 000000000..bdd321cb4
--- /dev/null
+++ b/tests/plugin/kawaguchi/InsertSort.scala
@@ -0,0 +1,39 @@
+package plugin.kawaguchi
+
+/* Example from paper "Type-based Data Structure Verification"
+ * http://pho.ucsd.edu/liquid/demo/index2.php */
+
+import funcheck.lib.Specs._
+
+object InsertSort {
+
+ def insert(ys: List[Int], x: Int): List[Int] = ys match {
+ case Nil => List(x)
+ case y :: ys =>
+ if (x < y) x :: y :: ys
+ else y :: insert(ys,x)
+ }
+
+ def insert_sort(xs: List[Int]): List[Int] = xs match {
+ case Nil => Nil
+ case x :: xs =>
+ insert(insert_sort(xs),x)
+ }
+
+ def insert_sort2(xs: List[Int]): List[Int] =
+ xs.foldLeft[List[Int]](Nil)((x,xs) => insert(x,xs))
+
+ 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(insert_sort(xs)) && check(insert_sort2(xs))
+
+ forAll{xs: List[Int] => test(xs)}
+
+ def main(args: Array[String]) = {}
+}
--
GitLab