Skip to content
Snippets Groups Projects
Commit 1591aef3 authored by Philippe Suter's avatar Philippe Suter
Browse files

Some additions, some refactoring, some fixes (incomplete commit).

parent e3b680a8
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 129 additions and 103 deletions
Test.scala
+ 6
− 2
View file @ 1591aef3
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)
}
build.xml
+ 44
− 77
View file @ 1591aef3
......@@ -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>
......
examples/contracts/heap/LeftistHeap.scala
+ 5
− 5
View file @ 1591aef3
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
}
scalac-plugin.xml
+ 1
− 1
View file @ 1591aef3
<plugin>
<name>funcheck</name>
<classname>funcheck.FunCheck</classname>
<classname>funcheck.FunCheckPlugin</classname>
</plugin>
src/funcheck/AnalysisPhase.scala → src/funcheck/AnalysisComponent.scala
+ 55
− 0
View file @ 1591aef3
......@@ -3,7 +3,7 @@ package funcheck
import scala.tools.nsc._
import scala.tools.nsc.plugins._
class AnalysisComponent(val global: Global, pluginInstance: FunCheck) extends PluginComponent {
class AnalysisComponent(val global: Global, val pluginInstance: FunCheckPlugin) extends PluginComponent with Extractors {
import global._
import global.definitions._
......@@ -16,10 +16,10 @@ class AnalysisComponent(val global: Global, pluginInstance: FunCheck) extends Pl
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)
import StructuralExtractors._
def apply(unit: CompilationUnit): Unit = {
(new ForeachTreeTraverser(findContracts)).traverse(unit.body)
if(pluginInstance.stopAfterAnalysis) {
println("Analysis complete. Now terminating the compiler process.")
......@@ -27,28 +27,29 @@ class AnalysisComponent(val global: Global, pluginInstance: FunCheck) extends Pl
}
}
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)
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 _ => ;
}
}
}
src/funcheck/FunCheck.scala → src/funcheck/FunCheckPlugin.scala
+ 1
− 1
View file @ 1591aef3
......@@ -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"
......
src/scala/collection/MultiSet.scala → src/scala/collection/Multiset.scala
+ 6
− 6
View file @ 1591aef3
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"
}
src/scala/collection/immutable/MultiSet.scala → src/scala/collection/immutable/Multiset.scala
+ 11
− 11
View file @ 1591aef3
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]
}
test.dmp deleted 100644 → 0
+ 0
− 0
View file @ e3b680a8
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment