Skip to content
Snippets Groups Projects
Commit 1c96089d authored by Mirco Dotta's avatar Mirco Dotta
Browse files

Specs implication is now working correctly. Arguments needed to be evaluated...

Specs implication is now working correctly. Arguments needed to be evaluated lazily. Now all properties in LeftistHeap can be checked correctly.
parent 6931e452
No related branches found
No related tags found
No related merge requests found
...@@ -10,8 +10,8 @@ object Specs { ...@@ -10,8 +10,8 @@ object Specs {
*/ */
class generator extends StaticAnnotation class generator extends StaticAnnotation
implicit def extendedBoolean(b: Boolean) = new { implicit def extendedBoolean(b: => Boolean) = new {
def ==>(p: Boolean) = (!b || p) // Specs ==> (b,p) def ==>(p: => Boolean) = Specs ==> (b,p)
} }
def forAll[A](f: A => Boolean): Boolean = { def forAll[A](f: A => Boolean): Boolean = {
...@@ -22,9 +22,5 @@ object Specs { ...@@ -22,9 +22,5 @@ object Specs {
/** Implication */ /** Implication */
/* def ==>(ifz: => Boolean, then: Boolean): Boolean = { def ==>(ifz: => Boolean, then: => Boolean): Boolean = !ifz || then
Console.err.println("Warning: ignored implication. Are you using the funcheck plugin?")
true
//error("\"==>\" (implication) combinator is currently unsupported by plugin.")
}*/
} }
...@@ -102,10 +102,10 @@ object LeftistHeap extends Application { ...@@ -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))) //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))} //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))} //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)))}
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment