diff --git a/examples/contracts/insertionsort/InsertionSort.scala b/examples/contracts/insertionsort/InsertionSort.scala new file mode 100644 index 0000000000000000000000000000000000000000..a262e326736fe69010c77fe77b23ae54c07f7293 --- /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 9cb880a382bff49893661a5fb195f18786552552..ba31e18884b95620a922d192267bfb21d7d6ef6a 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.") + } }