From 648a0e464a82a1bc2f266f77fbda2f3c5c14a1d5 Mon Sep 17 00:00:00 2001
From: Mirco Dotta <mirco.dotta@gmail.com>
Date: Mon, 13 Jul 2009 15:31:53 +0000
Subject: [PATCH] Small changes (mostly comments and formatting).
---
tests/plugin/BST.scala | 3 +-
tests/plugin/ConsSnoc.scala | 4 +--
tests/plugin/LambdaEvaluator.scala | 42 ++++++++++++++-------------
tests/plugin/LeftistHeap.scala | 6 ++--
tests/plugin/ListSet.scala | 7 ++---
tests/plugin/PropositionalLogic.scala | 29 ++----------------
tests/plugin/SetRedBlackTree.scala | 5 ++--
7 files changed, 38 insertions(+), 58 deletions(-)
diff --git a/tests/plugin/BST.scala b/tests/plugin/BST.scala
index 09ed9cb80..c453014a3 100644
--- a/tests/plugin/BST.scala
+++ b/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]) = {}
}
diff --git a/tests/plugin/ConsSnoc.scala b/tests/plugin/ConsSnoc.scala
index 017347d28..ace4da4d3 100644
--- a/tests/plugin/ConsSnoc.scala
+++ b/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
diff --git a/tests/plugin/LambdaEvaluator.scala b/tests/plugin/LambdaEvaluator.scala
index 8f0686f76..92e45ff76 100644
--- a/tests/plugin/LambdaEvaluator.scala
+++ b/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))))
+// )
}
+
}
diff --git a/tests/plugin/LeftistHeap.scala b/tests/plugin/LeftistHeap.scala
index c1835f588..5dd2ceae0 100644
--- a/tests/plugin/LeftistHeap.scala
+++ b/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]) = {}
}
diff --git a/tests/plugin/ListSet.scala b/tests/plugin/ListSet.scala
index 7035c7ddc..3937c1016 100644
--- a/tests/plugin/ListSet.scala
+++ b/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 = {}
}
diff --git a/tests/plugin/PropositionalLogic.scala b/tests/plugin/PropositionalLogic.scala
index fa65beee3..db1195a34 100644
--- a/tests/plugin/PropositionalLogic.scala
+++ b/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]) = {}
}
diff --git a/tests/plugin/SetRedBlackTree.scala b/tests/plugin/SetRedBlackTree.scala
index 21d3bab53..77787ed54 100644
--- a/tests/plugin/SetRedBlackTree.scala
+++ b/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]) = {}
}
--
GitLab