From dab3710c926b237d433be159ecb961e4a952c8f4 Mon Sep 17 00:00:00 2001
From: Mirco Dotta <mirco.dotta@gmail.com>
Date: Tue, 14 Jul 2009 09:28:53 +0000
Subject: [PATCH] reorganized folders and updated scripts accordingly.
---
.classpath | 1 +
Test1.scala | 16 +-
Test4.scala | 49 +++++-
build.xml | 161 +++++++++---------
{tests/plugin => examples/funcheck}/BST.scala | 2 +-
.../funcheck}/ConsSnoc.scala | 2 +-
.../funcheck}/LambdaEvaluator.scala | 2 +-
.../funcheck}/LeftistHeap.scala | 2 +-
.../funcheck}/ListSet.scala | 2 +-
.../funcheck}/PropositionalLogic.scala | 2 +-
.../funcheck}/SetRedBlackTree.scala | 2 +-
.../kawaguchi_pldi2010}/InsertSort.scala | 2 +-
.../kawaguchi_pldi2010}/MapReduce.scala | 2 +-
.../kawaguchi_pldi2010}/MergeSort.scala | 2 +-
.../kawaguchi_pldi2010}/MergeSortBug.scala | 2 +-
.../kawaguchi_pldi2010}/MiniBDD.scala | 2 +-
.../kawaguchi_pldi2010}/PosSplayHeap.scala | 0
.../kawaguchi_pldi2010}/QuickSort.scala | 2 +-
.../kawaguchi_pldi2010}/SplayHeap.scala | 2 +-
forall-tests.sh | 56 +++---
.../scalacheck}/BSTSpec.scala | 2 +-
.../scalacheck}/DPLLSpec.scala | 2 +-
.../scalacheck}/LeftistHeapSpec.scala | 15 +-
.../scalatest}/DPLLTest.scala | 0
.../scalatest}/LeftistHeapSpec.scala | 0
.../collection}/MultisetSpec.scala | 0
26 files changed, 184 insertions(+), 146 deletions(-)
rename {tests/plugin => examples/funcheck}/BST.scala (98%)
rename {tests/plugin => examples/funcheck}/ConsSnoc.scala (99%)
rename {tests/plugin => examples/funcheck}/LambdaEvaluator.scala (99%)
rename {tests/plugin => examples/funcheck}/LeftistHeap.scala (99%)
rename {tests/plugin => examples/funcheck}/ListSet.scala (98%)
rename {tests/plugin => examples/funcheck}/PropositionalLogic.scala (98%)
rename {tests/plugin => examples/funcheck}/SetRedBlackTree.scala (99%)
rename {tests/plugin/kawaguchi => examples/funcheck/kawaguchi_pldi2010}/InsertSort.scala (96%)
rename {tests/plugin/kawaguchi => examples/funcheck/kawaguchi_pldi2010}/MapReduce.scala (98%)
rename {tests/plugin/kawaguchi => examples/funcheck/kawaguchi_pldi2010}/MergeSort.scala (96%)
rename {tests/plugin/kawaguchi => examples/funcheck/kawaguchi_pldi2010}/MergeSortBug.scala (96%)
rename {tests/plugin/kawaguchi => examples/funcheck/kawaguchi_pldi2010}/MiniBDD.scala (99%)
rename {tests/plugin/kawaguchi => examples/funcheck/kawaguchi_pldi2010}/PosSplayHeap.scala (100%)
rename {tests/plugin/kawaguchi => examples/funcheck/kawaguchi_pldi2010}/QuickSort.scala (96%)
rename {tests/plugin/kawaguchi => examples/funcheck/kawaguchi_pldi2010}/SplayHeap.scala (98%)
rename tests/{scalacheck/examples => contracts/scalacheck}/BSTSpec.scala (98%)
rename tests/{scalacheck/examples => contracts/scalacheck}/DPLLSpec.scala (99%)
rename tests/{scalacheck/examples => contracts/scalacheck}/LeftistHeapSpec.scala (88%)
rename tests/{scalatest/examples => contracts/scalatest}/DPLLTest.scala (100%)
rename tests/{scalatest/examples => contracts/scalatest}/LeftistHeapSpec.scala (100%)
rename tests/{scalatest/examples => scala/collection}/MultisetSpec.scala (100%)
diff --git a/.classpath b/.classpath
index f8c97a1a5..3d4833db0 100644
--- a/.classpath
+++ b/.classpath
@@ -9,5 +9,6 @@
<classpathentry kind="lib" path="lib/scalatest-0.9.5.jar"/>
<classpathentry kind="lib" path="lib/specs-1.5.0.jar"/>
<classpathentry kind="lib" path="lib/ScalaCheck-1.5.jar" sourcepath="lib/ScalaCheck-1.5-src.jar"/>
+ <classpathentry combineaccessrules="false" kind="src" path="/scalacheck-read-only"/>
<classpathentry kind="output" path="bin"/>
</classpath>
diff --git a/Test1.scala b/Test1.scala
index 6cd5734cd..89b0d32b0 100644
--- a/Test1.scala
+++ b/Test1.scala
@@ -1,7 +1,8 @@
-import funcheck.lib.Specs._
-import org.scalacheck.{Gen, Arbitrary}
+import funcheck.lib.Specs
+import funcheck.lib.Specs.generator
+import org.scalacheck.{Gen, Arbitrary,Prop}
-object HeapTest {
+object HeapTest extends Application {
sealed abstract class Middle extends Top
case class E() extends Middle
@generator sealed abstract class Top
@@ -23,5 +24,12 @@ object HeapTest {
implicit def arbE: Arbitrary[E] = Arbitrary(Gen.oneOf(genE,genE2))
- forAll[(Elem,Elem,Int)]( p => 1+1 == 2)
+ Specs.forAll[(Int,Int)]( p => p._1 + p._2 == p._2 + p._1 )
+
+ //Specs.forAll[Int]( p => p == p)
+ Prop.forAll((a: Int,b: Int) => a+b == b+a)
+ Prop.forAll((a: Int,b: Int, c: Int) => a+b+c == b+a+c)
+
+
+ Prop.forAll((a: E) => a == a)
}
\ No newline at end of file
diff --git a/Test4.scala b/Test4.scala
index 7bece8d4d..32789c7de 100644
--- a/Test4.scala
+++ b/Test4.scala
@@ -1,12 +1,51 @@
-import funcheck.lib.Specs
+
object HeapTest extends Application {
-
+
+ /*
+ import org.scalacheck.Prop
+ import org.scalacheck.Prop._
+ forAll{(l1: List[Int], l2: List[Int]) => (l1 ++ l2).size == l1.size + l2.size}
+ */
+
+
+ //import funcheck.lib.Specs._
+// import org.scalacheck.Prop._
+// import org.scalacheck.Test.check
+// val prop = forAll{ p: Int => forAll{ v: Int => v + p == p + v}}
+// check(prop)
+
+ //import org.scalacheck.Prop._
+ import funcheck.lib.Specs._
+ forAll{ p: Int => forAll{ v: Int => v + p == p + v}}
+// forAll[(Int,Int)]{it=> true}
+// forAll{it: List[Int] => true}
+
+
+ //forAll[(Array[Int], Array[Int])]{ lists => (lists._1 ++ lists._2).size == lists._1.size + lists._2.size}
+
+
+ //val p = 3
+
+// import org.scalacheck.Prop._
+// import org.scalacheck.ConsoleReporter.testStatsEx
+// import org.scalacheck.Test.check
+
+ //p >= 0 ==> p > 0
+
+
+ //forAll{ p: Int => p > 1 ==> p >= 0}
+
+// val prop = forAll{ p: Int => p > 1 ==> p >= 0}
+// testStatsEx(check(prop))
+ //Prop.forAll{ p: Int => Prop.==>(p >= 0, p > 0)}
+
//works
- Specs.forAll[(Int,Int)]( p => p._1 + p._2 == p._2 + p._1)
+// forAll[Int]( p => forAll[Int]( v => v + p == p + v))
+// forAll[(Int,Int)]( p => p._1 + p._2 == p._2 + p._1)
//fails!
- Specs.forAll[Int]( p => p == 0)
-
+// forAll[Int]( p => p == 0)
+
}
\ No newline at end of file
diff --git a/build.xml b/build.xml
index 2cf215880..1f4340a4d 100644
--- a/build.xml
+++ b/build.xml
@@ -16,20 +16,23 @@
<property name="sources.dir" value="${base.dir}/src" />
<property name="examples.dir" value="${base.dir}/examples" />
<property name="tests.dir" value="${base.dir}/tests" />
- <property name="build.dir" value="${base.dir}/bin" />
<property name="dist.dir" value="${base.dir}/dist" />
-
<property name="lib.dir" value="${basedir}/lib" />
+ <property name="build.dir" value="${base.dir}/bin" />
+ <property name="build.plugin.funcheck.dir" value="${build.dir}/plugin" />
+ <property name="build.funcheck.lib.dir" value="${build.dir}/lib" />
+ <property name="build.scala.lib.extension.dir" value="${build.dir}/scala" />
<property name="build.examples.dir" value="${build.dir}/examples" />
<property name="build.tests.dir" value="${build.dir}/tests" />
+
<!-- other properties -->
<property name="dist.jar" value="${dist.dir}/funcheck-plugin.jar" />
<property name="main.class" value="funcheck.DefaultMain" />
<property name="script.file" value="${base.dir}/scalac-funcheck" />
<property name="scalac.default.params" value="-deprecation -unchecked" />
- <property name="scalac.funcheck.plugin" value="-Xplugin:${dist.jar}"/>
+ <property name="scalac.funcheck.plugin" value="-Xplugin:${dist.jar} ${scalac.default.params}"/>
<!-- required to use the tasks scalac, fsc and scaladoc -->
<taskdef resource="scala/tools/ant/antlib.xml">
@@ -45,86 +48,107 @@
<pathelement location="${scala-compiler.jar}" />
</path>
+ <path id="funcheck.lib.path">
+ <pathelement location="${build.funcheck.lib.dir}"/>
+ </path>
+
+ <path id="scala.lib.extension.path">
+ <pathelement location="${build.scala.lib.extension.dir}"/>
+ </path>
+
+
<path id="build.path">
<path refid="scalac.class.path"/>
- <pathelement location="${build.dir}" />
+ <path refid="funcheck.lib.path"/>
+ <pathelement location="${build.plugin.funcheck.dir}" />
</path>
- <!-- generic classpath settings (collecting all) -->
- <path id="lib.path">
- <pathelement location="${lib.dir}/ScalaCheck-1.5.jar"/>
+ <path id="scalacheck.lib.path">
+ <pathelement location="${lib.dir}/ScalaCheck-1.5.jar"/>
+ </path>
+
+ <path id="test.lib.path">
+ <path refid="scalacheck.lib.path"/>
<pathelement location="${lib.dir}/scalatest-0.9.5.jar" />
<pathelement location="${lib.dir}/specs-1.5.0.jar" />
-
- <!-- why the jars are not taken automatically from the lib .. ???
- <fileset dir=".">
- <include name="${lib.dir}/*.jar"/>
- </fileset>
- <fileset dir=".">
- <include name="${lib.dir}/*.zip"/>
- </fileset-->
</path>
+ <!-- phases definitions -->
+ <target name="compile-funcheck-lib" description="compile the FunCheck library (used for specification)">
+ <mkdir dir="${build.funcheck.lib.dir}" />
+ <scalac srcdir="${sources.dir}" destdir="${build.funcheck.lib.dir}" force="changed" addparams="${scalac.default.params}">
+ <classpath>
+ <path refid="scalac.class.path" />
+ </classpath>
+ <include name="funcheck/lib/**/*.scala" />
+ </scalac>
+ </target>
+
- <target name="compile" description="compile the FunCheck plugin">
- <mkdir dir="${build.dir}" />
- <scalac srcdir="${sources.dir}" destdir="${build.dir}" force="changed" addparams="${scalac.default.params}">
+ <target name="compile-scalac-lib-extension" description="compile Scala library extension for immutable Multiset">
+ <mkdir dir="${build.scala.lib.extension.dir}" />
+ <scalac srcdir="${sources.dir}" destdir="${build.scala.lib.extension.dir}" force="changed" addparams="${scalac.default.params}">
+ <classpath refid="scalac.class.path" />
+ <include name="scala/collection/**/*.scala" />
+ </scalac>
+ </target>
+
+
+ <target name="compile" depends="compile-funcheck-lib, compile-scalac-lib-extension" description="compile the FunCheck plugin">
+ <mkdir dir="${build.plugin.funcheck.dir}" />
+ <scalac srcdir="${sources.dir}" destdir="${build.plugin.funcheck.dir}" force="changed" addparams="${scalac.default.params}">
<classpath>
- <path refid="build.path" />
+ <path refid="scalac.class.path" />
</classpath>
- <include name="**/*.scala" />
<exclude name="scala/collection/**/*.scala"/>
+ <exclude name="funcheck/lib/**/*.scala"/>
</scalac>
</target>
- <target name="compile-lib-extension" description="compile Scala library extension for MultiSet">
- <mkdir dir="${build.dir}" />
- <scalac srcdir="${sources.dir}" destdir="${build.dir}" force="changed" addparams="${scalac.default.params}">
- <classpath refid="build.path" />
- <include name="scala/collection/**/*.scala" />
- </scalac>
+
+ <target name="dist" depends="compile" description="build the FunCheck jar file and create the script file used to run scalac with FunCheck plugged-in">
+ <mkdir dir="${dist.dir}" />
+
+ <manifest file="${dist.dir}/MANIFEST.MF">
+ <attribute name="Built-By" value="lara.epfl.ch" />
+ <attribute name="Main-Class" value="${main.class}" />
+ </manifest>
+
+ <jar destfile="${dist.jar}" manifest="${dist.dir}/MANIFEST.MF">
+ <fileset dir="${build.dir}" />
+ <fileset file="./scalac-plugin.xml" />
+ </jar>
+
+ <echo file="${script.file}" message="#!/bin/sh${line.separator}scalac -Xplugin:${dist.jar} $@${line.separator}" />
+ <chmod file="${script.file}" perm="u+x" />
</target>
- <target name="compile-examples" depends="compile, compile-lib-extension" description="compile the examples">
+ <target name="compile-examples" depends="dist" description="compile the examples">
<mkdir dir="${build.examples.dir}" />
<scalac srcdir="${examples.dir}" destdir="${build.examples.dir}" force="changed" addparams="${scalac.default.params}">
<classpath>
- <path refid="scalac.class.path" />
- <!-- To be precise, in the classpatht we should have the
- funcheck/lib and the scala multiset library -->
- <path refid="build.path"/>
+ <path refid="scala.lib.extension.path" />
+ <path refid="build.path" />
+ <path refid="scalacheck.lib.path" />
</classpath>
</scalac>
</target>
- <target name="compile-all" depends="compile,compile-examples" description="compile FunCheck and the examples" />
+ <target name="compile-all" depends="compile-tests" description="compile FunCheck, create a distribution file, compile examples and tests" />
- <target name="compile-tests-examples" depends="compile-examples" description="compile the suite tests for the examples">
+ <target name="compile-tests" depends="compile-examples" description="compile the tests suite">
<mkdir dir="${build.tests.dir}" />
<scalac srcdir="${tests.dir}" destdir="${build.tests.dir}" force="changed" addparams="${scalac.default.params}">
<classpath>
- <path refid="scalac.class.path" />
- <path refid="lib.path" />
+ <path refid="scala.lib.extension.path" />
+ <path refid="test.lib.path" />
<path refid="build.path" />
<pathelement location="${build.examples.dir}"/>
</classpath>
- <exclude name="plugin/**/*.scala" />
</scalac>
</target>
- <!--target name="compile-funcheck-tests" depends="compile, compile-lib-extension, dist" description="compile tests that use the FunCheck library">
- <mkdir dir="${build.tests.dir}" />
- <scalac srcdir="${tests.dir}" destdir="${build.tests.dir}" force="changed" addparams="${scalac.funcheck.plugin}">
- <classpath>
- <path refid="scalac.class.path" />
- <path refid="lib.path" />
- <path refid="build.path"/>
- </classpath>
- <include name="plugin/*.scala" />
- </scalac>
- </target-->
-
- <target name="run-test" depends="compile-tests-examples"
+ <target name="run-test" depends="compile-tests"
description="run a test (test name is provided by the user)">
<input message="Please enter the name of the test you want to run
(e.g., package_name.ClassName)"
@@ -134,8 +158,8 @@
<echo message="--- running test ${test.name}."/>
<java classname="scala.tools.nsc.MainGenericRunner" fork="true">
<classpath>
- <path refid="scalac.class.path" />
- <path refid="lib.path" />
+ <path refid="scala.lib.extension.path" />
+ <path refid="test.lib.path" />
<path refid="build.path" />
<pathelement location="${build.examples.dir}"/>
<pathelement location="${build.tests.dir}"/>
@@ -144,32 +168,13 @@
</java>
</target>
-
- <target name="dist" depends="compile, compile-lib-extension" description="build the FunCheck jar file and create the script file used to run scalac with FunCheck plugged-in">
- <mkdir dir="${dist.dir}" />
-
- <manifest file="${dist.dir}/MANIFEST.MF">
- <attribute name="Built-By" value="lara.epfl.ch" />
- <attribute name="Main-Class" value="${main.class}" />
- </manifest>
-
- <jar destfile="${dist.jar}" manifest="${dist.dir}/MANIFEST.MF">
- <fileset dir="${build.dir}" />
- <fileset file="./scalac-plugin.xml" />
- </jar>
-
- <echo file="${script.file}" message="#!/bin/sh${line.separator}scalac -Xplugin:${dist.jar} $@${line.separator}" />
- <chmod file="${script.file}" perm="u+x" />
- </target>
-
- <target name="clean" description="clean the project space">
- <delete file="${script.file}" quiet="yes" failonerror="no" />
- <delete dir="${build.dir}" includeemptydirs="yes" quiet="yes" failonerror="no" />
- <delete dir="${dist.dir}" includeemptydirs="yes" quiet="yes" failonerror="no" />
- <delete>
- <fileset dir="${basedir}" includes="**/*.class" />
- </delete>
- </target>
-
+ <target name="clean" description="clean the project space">
+ <delete file="${script.file}" quiet="yes" failonerror="no" />
+ <delete dir="${build.dir}" includeemptydirs="yes" quiet="yes" failonerror="no" />
+ <delete dir="${dist.dir}" includeemptydirs="yes" quiet="yes" failonerror="no" />
+ <delete>
+ <fileset dir="${basedir}" includes="**/*.class" />
+ </delete>
+ </target>
<target name="new" description="clean and rebuilds" depends="clean, dist" />
</project>
diff --git a/tests/plugin/BST.scala b/examples/funcheck/BST.scala
similarity index 98%
rename from tests/plugin/BST.scala
rename to examples/funcheck/BST.scala
index c453014a3..52ee8c8e7 100644
--- a/tests/plugin/BST.scala
+++ b/examples/funcheck/BST.scala
@@ -1,4 +1,4 @@
-package plugin
+package funcheck
import funcheck.lib.Specs._
diff --git a/tests/plugin/ConsSnoc.scala b/examples/funcheck/ConsSnoc.scala
similarity index 99%
rename from tests/plugin/ConsSnoc.scala
rename to examples/funcheck/ConsSnoc.scala
index ace4da4d3..d85a67595 100644
--- a/tests/plugin/ConsSnoc.scala
+++ b/examples/funcheck/ConsSnoc.scala
@@ -1,4 +1,4 @@
-package plugin
+package funcheck
import funcheck.lib.Specs._
diff --git a/tests/plugin/LambdaEvaluator.scala b/examples/funcheck/LambdaEvaluator.scala
similarity index 99%
rename from tests/plugin/LambdaEvaluator.scala
rename to examples/funcheck/LambdaEvaluator.scala
index 92e45ff76..ddf2b55fc 100644
--- a/tests/plugin/LambdaEvaluator.scala
+++ b/examples/funcheck/LambdaEvaluator.scala
@@ -1,4 +1,4 @@
-package plugin
+package funcheck
/** =================================================
* Evaluator for the untyped lambda calculus using
diff --git a/tests/plugin/LeftistHeap.scala b/examples/funcheck/LeftistHeap.scala
similarity index 99%
rename from tests/plugin/LeftistHeap.scala
rename to examples/funcheck/LeftistHeap.scala
index 5dd2ceae0..95f985ad3 100644
--- a/tests/plugin/LeftistHeap.scala
+++ b/examples/funcheck/LeftistHeap.scala
@@ -1,4 +1,4 @@
-package plugin
+package funcheck
import funcheck.lib.Specs._
import scala.collection.immutable._
diff --git a/tests/plugin/ListSet.scala b/examples/funcheck/ListSet.scala
similarity index 98%
rename from tests/plugin/ListSet.scala
rename to examples/funcheck/ListSet.scala
index 3937c1016..b212c2697 100644
--- a/tests/plugin/ListSet.scala
+++ b/examples/funcheck/ListSet.scala
@@ -1,4 +1,4 @@
-package plugin
+package funcheck
import scala.collection.immutable.Set
import funcheck.lib.Specs._
diff --git a/tests/plugin/PropositionalLogic.scala b/examples/funcheck/PropositionalLogic.scala
similarity index 98%
rename from tests/plugin/PropositionalLogic.scala
rename to examples/funcheck/PropositionalLogic.scala
index db1195a34..77745aa66 100644
--- a/tests/plugin/PropositionalLogic.scala
+++ b/examples/funcheck/PropositionalLogic.scala
@@ -1,4 +1,4 @@
-package plugin
+package funcheck
import funcheck.lib.Specs._
diff --git a/tests/plugin/SetRedBlackTree.scala b/examples/funcheck/SetRedBlackTree.scala
similarity index 99%
rename from tests/plugin/SetRedBlackTree.scala
rename to examples/funcheck/SetRedBlackTree.scala
index 77787ed54..8716b0edf 100644
--- a/tests/plugin/SetRedBlackTree.scala
+++ b/examples/funcheck/SetRedBlackTree.scala
@@ -1,4 +1,4 @@
-package plugin
+package funcheck
import funcheck.lib.Specs._
diff --git a/tests/plugin/kawaguchi/InsertSort.scala b/examples/funcheck/kawaguchi_pldi2010/InsertSort.scala
similarity index 96%
rename from tests/plugin/kawaguchi/InsertSort.scala
rename to examples/funcheck/kawaguchi_pldi2010/InsertSort.scala
index bdd321cb4..bfc6361e6 100644
--- a/tests/plugin/kawaguchi/InsertSort.scala
+++ b/examples/funcheck/kawaguchi_pldi2010/InsertSort.scala
@@ -1,4 +1,4 @@
-package plugin.kawaguchi
+package funcheck.kawaguchi_pldi2010
/* Example from paper "Type-based Data Structure Verification"
* http://pho.ucsd.edu/liquid/demo/index2.php */
diff --git a/tests/plugin/kawaguchi/MapReduce.scala b/examples/funcheck/kawaguchi_pldi2010/MapReduce.scala
similarity index 98%
rename from tests/plugin/kawaguchi/MapReduce.scala
rename to examples/funcheck/kawaguchi_pldi2010/MapReduce.scala
index beba264d6..5d68c2ae4 100644
--- a/tests/plugin/kawaguchi/MapReduce.scala
+++ b/examples/funcheck/kawaguchi_pldi2010/MapReduce.scala
@@ -1,4 +1,4 @@
-package plugin.kawaguchi
+package funcheck.kawaguchi_pldi2010
/* Example from paper "Type-based Data Structure Verification"
* http://pho.ucsd.edu/liquid/demo/index2.php */
diff --git a/tests/plugin/kawaguchi/MergeSort.scala b/examples/funcheck/kawaguchi_pldi2010/MergeSort.scala
similarity index 96%
rename from tests/plugin/kawaguchi/MergeSort.scala
rename to examples/funcheck/kawaguchi_pldi2010/MergeSort.scala
index 4c3f4b5d8..4cb78417a 100644
--- a/tests/plugin/kawaguchi/MergeSort.scala
+++ b/examples/funcheck/kawaguchi_pldi2010/MergeSort.scala
@@ -1,4 +1,4 @@
-package plugin.kawaguchi
+package funcheck.kawaguchi_pldi2010
import funcheck.lib.Specs._
diff --git a/tests/plugin/kawaguchi/MergeSortBug.scala b/examples/funcheck/kawaguchi_pldi2010/MergeSortBug.scala
similarity index 96%
rename from tests/plugin/kawaguchi/MergeSortBug.scala
rename to examples/funcheck/kawaguchi_pldi2010/MergeSortBug.scala
index bd2b245bf..a9e735715 100644
--- a/tests/plugin/kawaguchi/MergeSortBug.scala
+++ b/examples/funcheck/kawaguchi_pldi2010/MergeSortBug.scala
@@ -1,4 +1,4 @@
-package plugin.kawaguchi
+package funcheck.kawaguchi_pldi2010
import funcheck.lib.Specs._
diff --git a/tests/plugin/kawaguchi/MiniBDD.scala b/examples/funcheck/kawaguchi_pldi2010/MiniBDD.scala
similarity index 99%
rename from tests/plugin/kawaguchi/MiniBDD.scala
rename to examples/funcheck/kawaguchi_pldi2010/MiniBDD.scala
index 26ed18d24..d9f0a643e 100644
--- a/tests/plugin/kawaguchi/MiniBDD.scala
+++ b/examples/funcheck/kawaguchi_pldi2010/MiniBDD.scala
@@ -1,4 +1,4 @@
-package plugin.kawaguchi
+package funcheck.kawaguchi_pldi2010
/* Example from paper "Type-based Data Structure Verification"
* http://pho.ucsd.edu/liquid/demo/index2.php */
diff --git a/tests/plugin/kawaguchi/PosSplayHeap.scala b/examples/funcheck/kawaguchi_pldi2010/PosSplayHeap.scala
similarity index 100%
rename from tests/plugin/kawaguchi/PosSplayHeap.scala
rename to examples/funcheck/kawaguchi_pldi2010/PosSplayHeap.scala
diff --git a/tests/plugin/kawaguchi/QuickSort.scala b/examples/funcheck/kawaguchi_pldi2010/QuickSort.scala
similarity index 96%
rename from tests/plugin/kawaguchi/QuickSort.scala
rename to examples/funcheck/kawaguchi_pldi2010/QuickSort.scala
index 57fd0fbaf..26db82d28 100644
--- a/tests/plugin/kawaguchi/QuickSort.scala
+++ b/examples/funcheck/kawaguchi_pldi2010/QuickSort.scala
@@ -1,4 +1,4 @@
-package plugin.kawaguchi
+package funcheck.kawaguchi_pldi2010
/* Example from paper "Type-based Data Structure Verification"
* http://pho.ucsd.edu/liquid/demo/index2.php */
diff --git a/tests/plugin/kawaguchi/SplayHeap.scala b/examples/funcheck/kawaguchi_pldi2010/SplayHeap.scala
similarity index 98%
rename from tests/plugin/kawaguchi/SplayHeap.scala
rename to examples/funcheck/kawaguchi_pldi2010/SplayHeap.scala
index 095a110e5..cb8ad0c8c 100644
--- a/tests/plugin/kawaguchi/SplayHeap.scala
+++ b/examples/funcheck/kawaguchi_pldi2010/SplayHeap.scala
@@ -1,4 +1,4 @@
-package plugin.kawaguchi
+package funcheck.kawaguchi_pldi2010
/* Example from paper "Type-based Data Structure Verification"
* http://pho.ucsd.edu/liquid/demo/index2.php */
diff --git a/forall-tests.sh b/forall-tests.sh
index 2e43c4467..ad544b5f7 100755
--- a/forall-tests.sh
+++ b/forall-tests.sh
@@ -61,27 +61,9 @@ echo
shopt -s expand_aliases;
-alias scalac=".././scalac-funcheck -cp ../bin:../lib/ScalaCheck-1.5.jar -d ../bin/tests"
+alias scalac="./scalac-funcheck"
-mkdir bin/tests
-cd tests
-
-scalac plugin/BST.scala
-scalac plugin/LeftistHeap.scala
-scalac plugin/ListSet.scala
-scalac plugin/LambdaEvaluator.scala
-scalac plugin/PropositionalLogic.scala
-scalac plugin/SetRedBlackTree.scala
-scalac plugin/ConsSnoc.scala
-
-scalac plugin/kawaguchi/InsertSort.scala
-scalac plugin/kawaguchi/MergeSort.scala
-scalac plugin/kawaguchi/MergeSortBug.scala
-scalac plugin/kawaguchi/QuickSort.scala
-scalac plugin/kawaguchi/MapReduce.scala
-scalac plugin/kawaguchi/SplayHeap.scala
-
-cd ..
+ant compile-examples
# Scala compiler with the Funcheck plugin integrated
#alias scalac="./scalac-funcheck"
@@ -96,23 +78,25 @@ echo "Running tests with forAll properties."
echo "********************************************************************************"
echo
-alias scala="scala -cp bin/:${SCALACHECK_JAR}:bin/tests/"
+export CP="bin/:${SCALACHECK_JAR}:dist/funcheck-plugin.jar:bin/scala:bin/examples/:bin/lib"
+alias scala="scala -cp ${CP}"
+
# examples
-export BST="plugin.BST"
-export LeftistHeap="plugin.LeftistHeap"
-export ListSet="plugin.ListSet"
-export LambdaEvaluator="plugin.LambdaEvaluator"
-export PropositionalLogic="plugin.PropositionalLogic"
-export SetRedBlackTree="plugin.SetRedBlackTree"
-export ConsSnoc="plugin.ConsSnoc"
-
-export InsertSort="plugin.kawaguchi.InsertSort"
-export MergeSort="plugin.kawaguchi.MergeSort"
-export MergeSortBug="plugin.kawaguchi.MergeSortBug"
-export QuickSort="plugin.kawaguchi.QuickSort"
-export MapReduce="plugin.kawaguchi.MapReduce"
-export SplayHeap="plugin.kawaguchi.SplayHeap"
+export BST="funcheck.BST"
+export LeftistHeap="funcheck.LeftistHeap"
+export ListSet="funcheck.ListSet"
+export LambdaEvaluator="funcheck.LambdaEvaluator"
+export PropositionalLogic="funcheck.PropositionalLogic"
+export SetRedBlackTree="funcheck.SetRedBlackTree"
+export ConsSnoc="funcheck.ConsSnoc"
+
+export InsertSort="funcheck.kawaguchi_pldi2010.InsertSort"
+export MergeSort="funcheck.kawaguchi_pldi2010.MergeSort"
+export MergeSortBug="funcheck.kawaguchi_pldi2010.MergeSortBug"
+export QuickSort="funcheck.kawaguchi_pldi2010.QuickSort"
+export MapReduce="funcheck.kawaguchi_pldi2010.MapReduce"
+export SplayHeap="funcheck.kawaguchi_pldi2010.SplayHeap"
echo " - Testing ${BST}"
scala ${BST}
@@ -126,7 +110,7 @@ scala ${ListSet}
echo " - Testing ${SetRedBlackTree}"
scala ${SetRedBlackTree}
-echo " - Testing ${LambdEvaluator}"
+echo " - Testing ${LambdaEvaluator}"
scala ${LambdaEvaluator}
echo " - Testing ${PropositionalLogic}"
diff --git a/tests/scalacheck/examples/BSTSpec.scala b/tests/contracts/scalacheck/BSTSpec.scala
similarity index 98%
rename from tests/scalacheck/examples/BSTSpec.scala
rename to tests/contracts/scalacheck/BSTSpec.scala
index 2e0b20f74..ee90b9b87 100644
--- a/tests/scalacheck/examples/BSTSpec.scala
+++ b/tests/contracts/scalacheck/BSTSpec.scala
@@ -1,4 +1,4 @@
-package scalacheck.examples
+package contracts
import org.scalacheck.{Arbitrary,Properties,Gen}
import org.scalacheck.Prop._
diff --git a/tests/scalacheck/examples/DPLLSpec.scala b/tests/contracts/scalacheck/DPLLSpec.scala
similarity index 99%
rename from tests/scalacheck/examples/DPLLSpec.scala
rename to tests/contracts/scalacheck/DPLLSpec.scala
index 34f1deb33..03f47614c 100644
--- a/tests/scalacheck/examples/DPLLSpec.scala
+++ b/tests/contracts/scalacheck/DPLLSpec.scala
@@ -1,4 +1,4 @@
-package scalacheck.examples
+package contracts
import org.scalacheck.{Arbitrary,Properties,Gen}
import org.scalacheck.Prop._
diff --git a/tests/scalacheck/examples/LeftistHeapSpec.scala b/tests/contracts/scalacheck/LeftistHeapSpec.scala
similarity index 88%
rename from tests/scalacheck/examples/LeftistHeapSpec.scala
rename to tests/contracts/scalacheck/LeftistHeapSpec.scala
index d7e3a9e31..ac86913f1 100644
--- a/tests/scalacheck/examples/LeftistHeapSpec.scala
+++ b/tests/contracts/scalacheck/LeftistHeapSpec.scala
@@ -1,4 +1,4 @@
-package scalacheck.examples
+package contracts
import org.scalacheck.{Arbitrary,Gen}
@@ -14,15 +14,14 @@ object LeftistHeapSpec {
import contracts.heap.LeftistHeap._
-
/**********************************************************/
/*********************** GENERATORS ***********************/
/**********************************************************/
- def genElem: Gen[Elem] = for(v <- arbitrary[Int]) yield Elem(v)
- def genE: Gen[Heap] = Gen.value(E)
- def genT: Gen[Heap] = for {
- e <- genElem
- h <- genHeap
+ val genElem = for(v <- arbitrary[Int]) yield Elem(v)
+ val genE = Gen.value(E)
+ val genT = for {
+ e <- arbitrary[Elem]
+ h <- arbitrary[Heap]
} yield h.insert(e)
def genHeap: Gen[Heap] = Gen.lzy(Gen.oneOf(genE,genT))
@@ -30,6 +29,8 @@ object LeftistHeapSpec {
implicit def arbHeap: Arbitrary[Heap] = Arbitrary(genHeap)
implicit def arbElem: Arbitrary[Elem] = Arbitrary(genElem)
+ println(genHeap.sample)
+ println(genHeap.sample)
/**********************************************************/
/*********************** PROPERTIES ***********************/
diff --git a/tests/scalatest/examples/DPLLTest.scala b/tests/contracts/scalatest/DPLLTest.scala
similarity index 100%
rename from tests/scalatest/examples/DPLLTest.scala
rename to tests/contracts/scalatest/DPLLTest.scala
diff --git a/tests/scalatest/examples/LeftistHeapSpec.scala b/tests/contracts/scalatest/LeftistHeapSpec.scala
similarity index 100%
rename from tests/scalatest/examples/LeftistHeapSpec.scala
rename to tests/contracts/scalatest/LeftistHeapSpec.scala
diff --git a/tests/scalatest/examples/MultisetSpec.scala b/tests/scala/collection/MultisetSpec.scala
similarity index 100%
rename from tests/scalatest/examples/MultisetSpec.scala
rename to tests/scala/collection/MultisetSpec.scala
--
GitLab