Small changes (mostly comments and formatting).

tests/plugin/BST.scala

@@ -2,7 +2,7 @@ package plugin
 
 import funcheck.lib.Specs._
 
-object BST extends Application {
+object BST {
   /** class hierarchy*/
   sealed abstract class BST
   @generator case class Empty() extends BST
@@ -50,5 +50,6 @@ object BST extends Application {
   forAll{ p: (BST,Int) => contains(p._2,p._1) == content(p._1).contains(p._2)}
   forAll{ p: (BST,Int) => content(add(p._2, p._1)) == content(p._1) + p._2}
   
+  def main(args: Array[String]) = {}
 }
 

tests/plugin/ConsSnoc.scala

@@ -51,7 +51,7 @@ object ConsSnoc {
     case Cons(x, Snoc(_,y)) => Cons(x,Cons(y,Nill()))
   }
   
-  def main(args: Array[String]) = {}
+ 
 
   
   // Nill extractor always succeed for Nill instances
@@ -100,5 +100,5 @@ object ConsSnoc {
     case _ => false
   }
   
-
+  def main(args: Array[String]) = {}
 }
\ No newline at end of file

tests/plugin/LambdaEvaluator.scala

@@ -30,17 +30,17 @@ object LambdaEvaluator {
   def isValue(that: Term): Boolean = that.isInstanceOf[Abstr]
   
   def reduceCallByValue(that: Term): Term = that match {
-      
-    case App(Abstr(t1:Term),v2:Term) if isValue(v2) =>
+    
+    case App(Abstr(t1), v2) if isValue(v2) =>
       subst(t1,1,v2)
   
-    case App(v1: Abstr, t2: Term) if !isValue(t2) =>
+    case App(v1: Abstr, t2) if !isValue(t2) =>
       App(v1, reduceCallByValue(t2))
 
-    case App(t1: Term, t2: Term) if !isValue(t1) =>
+    case App(t1, t2) if !isValue(t1) =>
       App(reduceCallByValue(t1), t2)
         
-    case Abstr(t1: Term) => Abstr(reduceCallByValue(t1))
+    case Abstr(t1) => Abstr(reduceCallByValue(t1))
     case Var(_) => that
     case Const() => that
   }
@@ -53,13 +53,14 @@ object LambdaEvaluator {
     
     case Abstr(t1: Term) => Abstr(subst(t1,index+1,s))
       
-    case App(t1: Term, t2: Term) =>
+    case App(t1, t2) =>
       App(subst(t1,index,s), subst(t2,index,s))
   }
   
-  // this fails (which is correct!)
-  // counter-example: p._1=Var(13) , p._2 = 13 , p._3 = Const()
   //forAll[(Term,Int,Term)]{p => p._1 == subst(subst(p._1,p._2,p._3),p._2,p._1)}
+  // this (correctly) fails 
+  // counter-example: p._1=Var(13) , p._2 = 13 , p._3 = Const()
+  
   
   
   def main(args: Array[String]) = {
@@ -71,20 +72,21 @@ object LambdaEvaluator {
      *   \\ 2 (\\ 1) that is \\z. z (\\x. x)
      *  =================================================
      */ 
-    assert(
-      reduce(
-        Abstr(
-          App(
-            Abstr(App(Var(1), Abstr(Var(1)))),
-            Abstr(App(Var(2),Var(1)))
-          )
-        )
-      )
-      ==
-      Abstr(App(Var(2), Abstr(Var(1))))
-    )
+//    assert(
+//      reduce(
+//        Abstr(
+//          App(
+//            Abstr(App(Var(1), Abstr(Var(1)))),
+//            Abstr(App(Var(2),Var(1)))
+//          )
+//        )
+//      )
+//      ==
+//      Abstr(App(Var(2), Abstr(Var(1))))
+//    )
   }
   
+  
 }
   
 

tests/plugin/LeftistHeap.scala

@@ -8,7 +8,7 @@ import scala.collection.immutable._
  * by Chris Okasaki.
  */ 
   
-object LeftistHeap extends Application {
+object LeftistHeap {
   
   /** method used for specification */
   def min(xs: List[Elem]): Elem = {
@@ -98,7 +98,7 @@ object LeftistHeap extends Application {
   //val heapInsert = forAll( (heap: Heap, value: Elem) => content(heap.insert(value))(value) == content(heap)(value) + 1)
   forAll[(Heap,Elem)]( p => content(insert(p._1,p._2))(p._2) == content(p._1)(p._2) + 1)
   
-  // This property should fail
+  // This property should (and does) fail
   //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))}
@@ -107,5 +107,7 @@ object LeftistHeap extends Application {
   
   //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)))}
+  
+  def main(args: Array[String]) = {}
 }
 

tests/plugin/ListSet.scala

@@ -38,10 +38,9 @@ object ListSet {
     case _ :: ys => member(x, ys)
   }
 
-  def main(args: Array[String]): Unit = {
-    println("Done.")
-  }
-
   //@generator 
   def makeNil: List[Int] = Nil
+  
+  
+  def main(args: Array[String]): Unit = {}
 }

tests/plugin/PropositionalLogic.scala

@@ -3,16 +3,8 @@ package plugin
 import funcheck.lib.Specs._
 
 object PropositionalLogic {
-  
-  
-
-  // This crash because there are too many non-terminals, and the automatically 
-  // injected generator may end up generating infinite formulas, which produce 
-  // java.lang.StackOverflowError
   @generator
   sealed abstract class Formula
-  // conjunction makes automatic generator crash
-  //case class And(left: Formula, right: Formula) extends Formula
   case class Or(left: Formula, right: Formula) extends Formula
   case class Neg(f: Formula) extends Formula
   case class True() extends Formula
@@ -20,19 +12,15 @@ object PropositionalLogic {
   case class Imply(left: Formula,right: Formula) extends Formula
 
 
- 
-  
   def desugar(f: Formula): Formula = f match {
     case True()            => f
     case False()           => f
-    //case And(left,right)   => And(desugar(left),desugar(right))
     case Or(left,right)    => Or(desugar(left),desugar(right))
     case Neg(f)            => Neg(desugar(f))
     case Imply(left,right) => Or(Neg(desugar(left)),desugar(right))
   }
   
   def isDesugared(f: Formula): Boolean = f match {
-    //case And(left,right)   => isDesugared(left) && isDesugared(right)
     case Or(left,right)    => isDesugared(left) && isDesugared(right)
     case Neg(f)            => isDesugared(f)
     case True()            => true
@@ -40,21 +28,10 @@ object PropositionalLogic {
     case i: Imply          => false
   }
   
+  //Type refinement: A desugarized formula does not contain an Imply node.
   forAll{f : Formula => isDesugared(f) ==> (desugar(f) == f) }
-  // the above forAll invariant replaces the below somewhat cummbersome Matcheck spec
-  /** Type refinement: A desugarized formula does not contain an Imply node.
-                       This condition must hold recursively over the whole tree
-  */
-  /* constraint (\forall f. f \in DesugaredFormula <-->
-                         ( f \in Tru |
-                           f \in Flse |
-                          (f \in Neg & Neg_getField_f(f) \in DesugaredFormula) |
-                          (f \in IOr & IOr_getField_left(f) \in DesugaredFormula & IOr_getField_right(f) \in DesugaredFormula) |
-                          (f \in IAnd & IAnd_getField_left(f) \in DesugaredFormula & IAnd_getField_right(f) \in DesugaredFormula)
-                         )) 
-  */
+  
     
-  def main(args: Array[String]) = 
-    assert(isDesugared(desugar(Imply(Imply(True(),False()),False()))))
+  def main(args: Array[String]) = {}
 }
 

tests/plugin/SetRedBlackTree.scala

@@ -57,9 +57,6 @@ object SetRedBlackTree {
     case _ => n
   }
   
-  
-  def main(args: Array[String]) = println("Done")
-  
   /* global invariants: 
    * Red-black trees are binary search trees obeying two key invariants:
    *
@@ -103,5 +100,7 @@ object SetRedBlackTree {
       areRedNodeChildrenBlack(l) && areRedNodeChildrenBlack(r)
     case _ => true
   }
+  
+  def main(args: Array[String]) = {}
 }