diff --git a/src/funcheck/lib/Specs.scala b/src/funcheck/lib/Specs.scala index 962ff5c571b8e9c33de40d96b4b4d692f041d7e4..1f3167cb6c596e518bb44d3fc47aa6455e317103 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 23cf0ced5c89929155070ce136256a250eee06c8..c1835f588233cf2a0c0c8be430a77ab9432f5264 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)))} }