From cd8784ac88d6bca34335b2d12cb770f00cefd6c6 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Thu, 18 Jun 2009 14:59:28 +0000
Subject: [PATCH] one more example, and Specs.forAll does not provoke a crash
at runtime anymore (a warning instead that its body has not been replaced by
the plugin)
---
.../insertionsort/InsertionSort.scala | 36 +++++++++++++++++++
src/funcheck/lib/Specs.scala | 15 +++++---
2 files changed, 46 insertions(+), 5 deletions(-)
create mode 100644 examples/contracts/insertionsort/InsertionSort.scala
diff --git a/examples/contracts/insertionsort/InsertionSort.scala b/examples/contracts/insertionsort/InsertionSort.scala
new file mode 100644
index 000000000..a262e3267
--- /dev/null
+++ b/examples/contracts/insertionsort/InsertionSort.scala
@@ -0,0 +1,36 @@
+package contracts.insertionsort
+
+import scala.collection.immutable.Set
+
+object InsertionSort {
+ import funcheck.lib.Specs
+
+ assert(
+ Specs.forAll(
+ (l: List[Int]) => { content(sorted(l)) equals content(l) }
+ )
+ )
+
+ def content(l: List[Int]): Set[Int] = l match {
+ case Nil => Set.empty
+ case x :: xs => content(xs) + x
+ }
+
+ def sortedIns(e: Int, l: List[Int]): List[Int] = l match {
+ case Nil => e :: Nil
+ case x :: xs if (x < e) => x :: sortedIns(e, xs)
+ case _ => e :: l
+ }
+
+ def sorted(l: List[Int]): List[Int] = l match {
+ case Nil => Nil
+ case x :: xs => sortedIns(x, sorted(xs))
+ }
+
+ def main(args: Array[String]): Unit = {
+ val ls: List[Int] = List(5, 2, 4, 5, 1, 8)
+
+ println(ls)
+ println(sorted(ls))
+ }
+}
diff --git a/src/funcheck/lib/Specs.scala b/src/funcheck/lib/Specs.scala
index 9cb880a38..ba31e1888 100644
--- a/src/funcheck/lib/Specs.scala
+++ b/src/funcheck/lib/Specs.scala
@@ -14,12 +14,17 @@ object Specs {
def ==>(p: Boolean) = Specs ==> (b,p)
}
- def forAll[A](f: A => Boolean): Boolean =
- error("\"forAll\" combinator is currently unsupported by plugin.")
+ def forAll[A](f: A => Boolean): Boolean = {
+ Console.err.println("Warning: ignored forAll. Are you using the funcheck plugin?")
+ true
+ // error("\"forAll\" combinator is currently unsupported by plugin.")
+ }
/** Implication */
- def ==>(ifz: => Boolean, then: Boolean): Boolean =
- error("\"==>\" (implication) combinator is currently unsupported by plugin.")
-
+ def ==>(ifz: => Boolean, then: Boolean): Boolean = {
+ Console.err.println("Warning: ignored implication. Are you using the funcheck plugin?")
+ true
+ //error("\"==>\" (implication) combinator is currently unsupported by plugin.")
+ }
}
--
GitLab