diff --git a/Test.scala b/Test.scala
index eaed15716fcad86035438a40399915a9ddc090fd..475902f071ef606441ff91afec957e7b500a9348 100644
--- a/Test.scala
+++ b/Test.scala
@@ -1,7 +1,11 @@
object Test {
def main(args: Array[String]): Unit = {
- require(2 == 2)
println("Ok")
- } ensuring (res => 2 == 2)
+ }
+
+ def useless(i: Int, j: Int): Int = {
+ require(i == j)
+ i + j
+ } ensuring(res => res == 2 * i)
}
diff --git a/build.xml b/build.xml
index ee011e73b10dc4f7069033ed4f7b9db85f240b46..eb069b09540381ac50d8094a09fbab6496a9c2e4 100644
--- a/build.xml
+++ b/build.xml
@@ -10,24 +10,25 @@
<property name="scala.home" value="${env.SCALA_HOME}" />
<property name="scala-library.jar" value="${scala.home}/lib/scala-library.jar" />
<property name="scala-compiler.jar" value="${scala.home}/lib/scala-compiler.jar" />
-
- <!-- folders -->
- <property name="base.dir" value="${basedir}" />
+
+ <!-- paths -->
+ <property name="base.dir" value="${basedir}" />
<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="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="lib.dir" value="${basedir}/lib" />
<property name="build.examples.dir" value="${build.dir}/examples" />
<property name="build.tests.dir" value="${build.dir}/tests" />
- <!-- other properties -->
+ <!-- other properties -->
<property name="dist.jar" value="${dist.dir}/funcheck-plugin.jar" />
- <property name="main.class" value="funcheck.DefaultMain" />
+ <property name="main.class" value="funcheck.DefaultMain" />
<property name="script.file" value="${base.dir}/scalac-funcheck" />
+ <property name="scalac.default.params" value="-deprecation -unchecked" />
<!-- required to use the tasks scalac, fsc and scaladoc -->
<taskdef resource="scala/tools/ant/antlib.xml">
@@ -41,99 +42,67 @@
<path id="scalac.class.path">
<pathelement location="${scala-library.jar}" />
<pathelement location="${scala-compiler.jar}" />
- </path>
+ </path>
<path id="build.path">
- <path refid="scalac.class.path"/>
+ <path refid="scalac.class.path"/>
<pathelement location="${build.dir}" />
</path>
<!-- generic classpath settings (collecting all) -->
- <path id="lib.path">
- <fileset dir=".">
- <include name="${lib.dir}/*.jar"/>
- </fileset>
- <fileset dir=".">
- <include name="${lib.dir}/*.zip"/>
- </fileset>
- </path>
-
-
+ <path id="lib.path">
+ <fileset dir=".">
+ <include name="${lib.dir}/*.jar"/>
+ </fileset>
+ <fileset dir=".">
+ <include name="${lib.dir}/*.zip"/>
+ </fileset>
+ </path>
- <!-- *
- * compile: it compiles all Funcheck's sources
- *-->
- <target name="compile" description="compile FunCheck">
+ <target name="compile" description="compile the FunCheck plugin">
<mkdir dir="${build.dir}" />
- <scalac srcdir="${sources.dir}" destdir="${build.dir}" force="changed" addparams="-deprecation">
+ <scalac srcdir="${sources.dir}" destdir="${build.dir}" force="changed" addparams="${scalac.default.params}">
<classpath refid="build.path" />
<include name="**/*.scala" />
- <exclude name="scala/collection/**/*.scala"/>
+ <exclude name="scala/collection/**/*.scala"/>
</scalac>
</target>
- <!-- *
- * compile-lib-extension: it compiles the library extension used to
- * define multiset
- *-->
<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="-deprecation">
+ <scalac srcdir="${sources.dir}" destdir="${build.dir}" force="changed" addparams="${scalac.default.params}">
<classpath refid="build.path" />
<include name="scala/collection/**/*.scala" />
</scalac>
</target>
-
- <!-- *
- *
- *-->
+
<target name="compile-examples" depends="compile-lib-extension" description="compile the examples">
<mkdir dir="${build.examples.dir}" />
- <scalac srcdir="${examples.dir}" destdir="${build.examples.dir}" force="changed"
- addparams="-deprecation">
- <classpath>
- <path refid="scalac.class.path" />
- <pathelement location="${build.dir}"/>
- </classpath>
- </scalac>
+ <scalac srcdir="${examples.dir}" destdir="${build.examples.dir}" force="changed" addparams="${scalac.default.params}">
+ <classpath>
+ <path refid="scalac.class.path" />
+ <pathelement location="${build.dir}"/>
+ </classpath>
+ </scalac>
</target>
+ <target name="compile-all" depends="compile,compile-examples" description="compile FunCheck and the examples" />
- <!-- *
- *
- *-->
- <target name="compile-all" depends="compile,compile-examples"
- description="compile FunCheck and the examples" />
-
-
-
- <!-- *
- *
- *-->
<target name="compile-tests-examples" depends="compile-examples" description="compile the suite tests for the examples">
- <mkdir dir="${build.tests.dir}" />
- <scalac srcdir="${tests.dir}" destdir="${build.tests.dir}" force="changed"
- addparams="-deprecation">
- <classpath>
- <path refid="scalac.class.path" />
- <path refid="lib.path" />
- <pathelement location="${lib.dir}/ScalaCheck-1.5.jar" />
- <pathelement location="${build.examples.dir}"/>
- </classpath>
- </scalac>
+ <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" />
+ <pathelement location="${lib.dir}/ScalaCheck-1.5.jar" />
+ <pathelement location="${build.examples.dir}"/>
+ </classpath>
+ </scalac>
</target>
-
-
-
- <!-- *
- *
- *-->
<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}" />
- <copy file="./scalac-plugin.xml" todir="${build.dir}" overwrite="true" />
-
<manifest file="${dist.dir}/MANIFEST.MF">
<attribute name="Built-By" value="lara.epfl.ch" />
<attribute name="Main-Class" value="${main.class}" />
@@ -141,21 +110,19 @@
<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 FunCheck">
+ <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="${examples.dir}" includes="**/*.class" />
+ <fileset dir="${basedir}" includes="**/*.class" />
</delete>
</target>
diff --git a/examples/contracts/heap/LeftistHeap.scala b/examples/contracts/heap/LeftistHeap.scala
index 12ad0f2ec411dc116474b0464c5fac83f38a2470..4e198484462cb3bdee4395b2c565141cd90a8b12 100644
--- a/examples/contracts/heap/LeftistHeap.scala
+++ b/examples/contracts/heap/LeftistHeap.scala
@@ -1,6 +1,6 @@
package contracts.heap
-import scala.collection.immutable.MultiSet
+import scala.collection.immutable.Multiset
/**
* Example adapted from book "Purely Functional Data Structures"
@@ -22,12 +22,12 @@ object Heap {
inner(xs,Elem(Integer.MAX_VALUE))
}
- private def content(t : Heap): MultiSet[Elem] = {
- def inner(t: Heap, mset: MultiSet[Elem]): MultiSet[Elem] = t match {
+ private def content(t : Heap): Multiset[Elem] = {
+ def inner(t: Heap, mset: Multiset[Elem]): Multiset[Elem] = t match {
case E => mset
case T(rank,el,left,right) => mset + el
}
- inner(t,MultiSet.empty[Elem])
+ inner(t,Multiset.empty[Elem])
}
}
@@ -109,4 +109,4 @@ object LeftistHeap extends Application {
.insert(new Elem(6))
//println(heap)
assert(heap.findMin.value == 4)
-}
\ No newline at end of file
+}
diff --git a/scalac-plugin.xml b/scalac-plugin.xml
index 53924d181ec26042c8d7f0af8d83aa1af2fb61b3..1d1af30471f802748863b3ae8ebc25734d9c581e 100644
--- a/scalac-plugin.xml
+++ b/scalac-plugin.xml
@@ -1,4 +1,4 @@
<plugin>
<name>funcheck</name>
- <classname>funcheck.FunCheck</classname>
+ <classname>funcheck.FunCheckPlugin</classname>
</plugin>
diff --git a/src/funcheck/AnalysisComponent.scala b/src/funcheck/AnalysisComponent.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3c365b88bffa9e5bbfad1640b0ca5a4f44d1a4d9
--- /dev/null
+++ b/src/funcheck/AnalysisComponent.scala
@@ -0,0 +1,55 @@
+package funcheck
+
+import scala.tools.nsc._
+import scala.tools.nsc.plugins._
+
+class AnalysisComponent(val global: Global, val pluginInstance: FunCheckPlugin) extends PluginComponent with Extractors {
+ import global._
+ import global.definitions._
+
+ // when we use 2.8.x, swap the following two lines
+ val runsAfter = "refchecks"
+ // override val runsRightAfter = "refchecks"
+
+ val phaseName = pluginInstance.name
+
+ def newPhase(prev: Phase) = new AnalysisPhase(prev)
+
+ class AnalysisPhase(prev: Phase) extends StdPhase(prev) {
+ import StructuralExtractors._
+
+ def apply(unit: CompilationUnit): Unit = {
+ (new ForeachTreeTraverser(findContracts)).traverse(unit.body)
+
+ if(pluginInstance.stopAfterAnalysis) {
+ println("Analysis complete. Now terminating the compiler process.")
+ exit(0)
+ }
+ }
+
+ def findContracts(tree: Tree): Unit = tree match {
+ case DefDef(/*mods*/ _, name, /*tparams*/ _, /*vparamss*/ _, /*tpt*/ _, body) => {
+ var realBody = body
+ var reqCont: Option[Tree] = None
+ var ensCont: Option[Function] = None
+
+ body match {
+ case EnsuredExpression(body2, contract) => realBody = body2; ensCont = Some(contract)
+ case _ => ;
+ }
+
+ realBody match {
+ case RequiredExpression(body3, contract) => realBody = body3; reqCont = Some(contract)
+ case _ => ;
+ }
+
+ println("In: " + name)
+ println(" Requires clause: " + reqCont)
+ println(" Ensures clause: " + ensCont)
+ println(" Body: " + realBody)
+ }
+
+ case _ => ;
+ }
+ }
+}
diff --git a/src/funcheck/AnalysisPhase.scala b/src/funcheck/AnalysisPhase.scala
deleted file mode 100644
index f3c85e4750f268e6fffea1bd6875afa5735ba185..0000000000000000000000000000000000000000
--- a/src/funcheck/AnalysisPhase.scala
+++ /dev/null
@@ -1,54 +0,0 @@
-package funcheck
-
-import scala.tools.nsc._
-import scala.tools.nsc.plugins._
-
-class AnalysisComponent(val global: Global, pluginInstance: FunCheck) extends PluginComponent {
- import global._
- import global.definitions._
-
- // when we use 2.8.x, swap the following two lines
- val runsAfter = "refchecks"
- // override val runsRightAfter = "refchecks"
-
- val phaseName = pluginInstance.name
-
- def newPhase(prev: Phase) = new AnalysisPhase(prev)
-
- class AnalysisPhase(prev: Phase) extends StdPhase(prev) {
- def apply(unit: CompilationUnit): Unit = {
- (new ForeachTreeTraverser(findDefs)).traverse(unit.body)
- (new ForeachTreeTraverser(findEnsurings)).traverse(unit.body)
-
-
- if(pluginInstance.stopAfterAnalysis) {
- println("Analysis complete. Now terminating the compiler process.")
- exit(0)
- }
- }
-
- def findDefs(tree: Tree): Unit = tree match {
- case d: DefDef => println("Found a def! : " + d)
- case _ => ;
- }
-
- def findEnsurings(tree: Tree): Unit = tree match {
- case DefDef(/*mods*/ _, name, /*tparams*/ _, /*vparamss*/ _, /*tpt*/ _,
- /* body */
- Apply(Select(Apply(TypeApply(Select(Select(This(scalaName), predefName), any2EnsuringName), TypeTree() :: Nil), body :: Nil), ensuringName), (anonymousFun @ Function(ValDef(_, resultName, resultType, EmptyTree) :: Nil, contractBody)) :: Nil) )
- if ( "scala".equals(scalaName.toString)
- && "Predef".equals(predefName.toString)
- && "any2Ensuring".equals(any2EnsuringName.toString)) => {
- println("Found a defdef with ensuring:")
- println("body: " + body)
- println("")
- println("cont: " + anonymousFun)
- println(resultName + " : " + resultType + " ==> " + contractBody)
-
- }
-
- case _ => ;
-
- }
- }
-}
diff --git a/src/funcheck/FunCheck.scala b/src/funcheck/FunCheckPlugin.scala
similarity index 94%
rename from src/funcheck/FunCheck.scala
rename to src/funcheck/FunCheckPlugin.scala
index 88d0ce29f46436ca4e9ba5aac0f4eb7732e007c0..9c1ad9a6df5c7f16210d02e3dd813f0d2e79a7fc 100644
--- a/src/funcheck/FunCheck.scala
+++ b/src/funcheck/FunCheckPlugin.scala
@@ -5,7 +5,7 @@ import scala.tools.nsc.{Global,Phase}
import scala.tools.nsc.plugins.{Plugin,PluginComponent}
/** This class is the entry point for the plugin. */
-class FunCheck(val global: Global) extends Plugin {
+class FunCheckPlugin(val global: Global) extends Plugin {
import global._
val name = "funcheck"
diff --git a/src/scala/collection/MultiSet.scala b/src/scala/collection/Multiset.scala
similarity index 87%
rename from src/scala/collection/MultiSet.scala
rename to src/scala/collection/Multiset.scala
index 572956568d5619b97874c61777442a5b7503bc6e..448b558e9f78d42ac9e93249b73a51612eca44ff 100644
--- a/src/scala/collection/MultiSet.scala
+++ b/src/scala/collection/Multiset.scala
@@ -1,7 +1,7 @@
package scala.collection
-trait MultiSet[A] extends (A => Int) with Collection[A]{
+trait Multiset[A] extends (A => Int) with Collection[A]{
/** Returns the number of elements in this multiset.
*
@@ -43,15 +43,15 @@ trait MultiSet[A] extends (A => Int) with Collection[A]{
* this multiset.
* todo: rename to isSubsetOf
*/
- def subsetOf(that: MultiSet[A]): Boolean =
- forall(e => apply(e) <= that.apply(e))
+ def subsetOf(that: Multiset[A]): Boolean =
+ forall(e => this(e) <= that(e))
/**
* This method is an alias for <code>intersect</code>. It computes an
* intersection with set that. It removes all the elements
* <code>that</code> are not present in that.
*/
- def ** (that: MultiSet[A]): MultiSet[A]
+ def ** (that: Multiset[A]): Multiset[A]
//structural equality
@@ -65,12 +65,12 @@ trait MultiSet[A] extends (A => Int) with Collection[A]{
* contain the same elements, with same cardinality.
*/
override def equals(that: Any): Boolean = that match {
- case other: MultiSet[A] => forall(e => apply(e) == other.apply(e))
+ case other: Multiset[_] => other.size == this.size && subsetOf(other.asInstanceOf[Multiset[A]])
case _ => false
}
/** Defines the prefix of this object's <code>toString</code> representation.
*/
- override protected def stringPrefix : String = "MultiSet"
+ override protected def stringPrefix : String = "Multiset"
}
diff --git a/src/scala/collection/immutable/MultiSet.scala b/src/scala/collection/immutable/Multiset.scala
similarity index 54%
rename from src/scala/collection/immutable/MultiSet.scala
rename to src/scala/collection/immutable/Multiset.scala
index 8619db840c90ec96d9db7cf5346262d8af013564..5b635cc41df429663d6e086c4c4ddd8895803255 100644
--- a/src/scala/collection/immutable/MultiSet.scala
+++ b/src/scala/collection/immutable/Multiset.scala
@@ -1,16 +1,16 @@
package scala.collection.immutable
-object MultiSet {
+object Multiset {
/** The empty set of this type */
- def empty[A]: MultiSet[A] = throw new UnsupportedOperationException("Concrete MultiSet classes need to be implemented")
+ def empty[A]: Multiset[A] = throw new UnsupportedOperationException("Concrete Multiset classes need to be implemented")
/** The canonical factory for this type */
- def apply[A](elems: A*): MultiSet[A] = empty[A] ++ elems
+ def apply[A](elems: A*): Multiset[A] = empty[A] ++ elems
}
-trait MultiSet[A] extends AnyRef with collection.MultiSet[A]{
+trait Multiset[A] extends AnyRef with collection.Multiset[A]{
/** This method is an alias for <code>intersect</code>.
* It computes an intersection with multiset <code>that</code>.
@@ -18,28 +18,28 @@ trait MultiSet[A] extends AnyRef with collection.MultiSet[A]{
*
* @param that the multiset to intersect with
*/
- override def ** (that: collection.MultiSet[A]): MultiSet[A] = intersect(that)
+ override def ** (that: collection.Multiset[A]): Multiset[A] = intersect(that)
/**
* This method computes an intersection with multiset that. It removes all
* the elements that are not present in that.
*/
- def intersect (that: collection.MultiSet[A]): MultiSet[A]
+ def intersect (that: collection.Multiset[A]): Multiset[A]
// A U elems (max)
- def ++ (elems: Iterable[A]): MultiSet[A]
+ def ++ (elems: Iterable[A]): Multiset[A]
// A U elems (sum)
- def +++ (elems: Iterable[A]): MultiSet[A]
+ def +++ (elems: Iterable[A]): Multiset[A]
// A \ {elems}
- def --(elems: Iterable[A]): MultiSet[A]
+ def --(elems: Iterable[A]): Multiset[A]
// A U {elems}
- def + (elems: A*): MultiSet[A]
+ def + (elems: A*): Multiset[A]
// A \ {elems}
- def - (elems: A*): MultiSet[A]
+ def - (elems: A*): Multiset[A]
def filter (p: A => Boolean): Iterable[A]
}
diff --git a/test.dmp b/test.dmp
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000