From 1c96089d51e85b3b40b646cd9378714fb464c991 Mon Sep 17 00:00:00 2001
From: Mirco Dotta <mirco.dotta@gmail.com>
Date: Mon, 13 Jul 2009 09:51:37 +0000
Subject: [PATCH] Specs implication is now working correctly. Arguments needed
to be evaluated lazily. Now all properties in LeftistHeap can be checked
correctly.
---
src/funcheck/lib/Specs.scala | 10 +++-------
tests/plugin/LeftistHeap.scala | 4 ++--
2 files changed, 5 insertions(+), 9 deletions(-)
diff --git a/src/funcheck/lib/Specs.scala b/src/funcheck/lib/Specs.scala
index 962ff5c57..1f3167cb6 100644
--- a/src/funcheck/lib/Specs.scala
+++ b/src/funcheck/lib/Specs.scala
@@ -10,8 +10,8 @@ object Specs {
*/
class generator extends StaticAnnotation
- implicit def extendedBoolean(b: Boolean) = new {
- def ==>(p: Boolean) = (!b || p) // Specs ==> (b,p)
+ implicit def extendedBoolean(b: => Boolean) = new {
+ def ==>(p: => Boolean) = Specs ==> (b,p)
}
def forAll[A](f: A => Boolean): Boolean = {
@@ -22,9 +22,5 @@ object Specs {
/** Implication */
-/* 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.")
- }*/
+ def ==>(ifz: => Boolean, then: => Boolean): Boolean = !ifz || then
}
diff --git a/tests/plugin/LeftistHeap.scala b/tests/plugin/LeftistHeap.scala
index 23cf0ced5..c1835f588 100644
--- a/tests/plugin/LeftistHeap.scala
+++ b/tests/plugin/LeftistHeap.scala
@@ -102,10 +102,10 @@ object LeftistHeap extends Application {
//forAll[(Heap,Elem)]( p => ((rankk(p._1) > 0 && findMin(p._1).value == p._2.value) ==> (findMin(p._1).value < p._2.value)))
//val heapFindMin = forAll{ heap : Heap => (heap.rankk > 0) ==> (heap.findMin == min(content(heap).elements.toList))}
- //forAll{ heap : Heap => (rankk(heap) > 0) ==> (findMin(heap) == min(content(heap).elements.toList))}
+ forAll{ heap : Heap => (rankk(heap) > 0) ==> (findMin(heap) == min(content(heap).elements.toList))}
//val heapDeleteMin = forAll{ heap: Heap => (heap.rankk > 0) ==> (content(heap.deleteMin).equals(content(heap) - heap.findMin))}
- //forAll{ heap: Heap => (rankk(heap) > 0) ==> (content(deleteMin(heap)).equals(content(heap) - findMin(heap)))}
+ forAll{ heap: Heap => (rankk(heap) > 0) ==> (content(deleteMin(heap)).equals(content(heap) - findMin(heap)))}
}
--
GitLab