================================================================================
===                             FUNCHECK PLUGIN                              ===       
================================================================================


COMPILE
======================


1 - Funcheck Plugin
----------------------

To compile the FunCheck project just type 'ant'. This will compile the 
scala.collection.immutable.Multiset library extension created as part of this 
project (Note: This should become a module in the future and then just have a 
jar file with the extended multiset collection). Furthermore, it will compile 
the internal funcheck.lib.Specs library used for declaring forAll properties 
in the examples. Finally, it will compile the plugin, create a distribution jar 
and also create a script 'scalac-funcheck' that should be used instead of 
the usual 'scalac' script for compiling examples of this project.  

2 - Funcheck Examples
----------------------

Examples that shows the functionality of the plugin are in the folder 'examples/plugin'
and also (for the static verification part) in 'examples/contracts'. To compile 
the former you should use the 'forall-tests' script, which will compile the examples
in the 'examples/plugin' directory and will also execute them. On the other hand, if you want 
to compile all the other examples you can simply type 'ant compile-examples'. 

XXX: We should really integrate the compilation of the examples in 'examples/plugin' 
into the 'forall-tests' script. However, this is not working right now (getting to 
crash the plugin extension when compile inside ant, while compilation outside ant works 
just fine. 

3 - Running Funcheck
----------------------

When the 'forall-tests' is launched, it will first compiles the examples in 'examples/plugin' 
and then it will execute them one after the other. You should see a similar output when the test
succeed:

+ OK, passed 100 tests.     //Nice!! This means the property was ok!

and this when it fails:

! Falsified after 1 passed tests.     //Ops, the property has been falsified                                        
> ARG_0: "1"
java.lang.ExceptionInInitializerError
	[...]
	

4 - Tests
----------------------

the 'tests' directory contains some unit tests for the examples and, most interestingly, 
an extensive test of the multiset collection library created as part of this project.  


================================================================================

OLD README:

Use:
    ant

...to compile the project.

Use:
    ant dist

...to generate the plugin jar file and a script to run scalac with the plugin.

Then, try for instance:
    ./scalac-funcheck -Xshow-phases

...and notice that funcheck runs right after refchecks. Note that
./scalac-funcheck is generated and contains the full path to the jar file, so
you can use it from any location and it will find what it needs. You may want
to symbolically link to it from ~/bin, for instance.

You can also try:
    ./scalac-funcheck -Xplugin-list

Try:
    ./scalac-funcheck Test.scala

...and notice that the plugin does something (in particular, the compilation
stops right after the plugin).

Try:
    ./scalac-funcheck -P:funcheck:with-code Test.scala

...to achieve the same result but with letting the compiler continue its work.

To clean up:
    ant clean

Useful for showing Scala AST
-----------------------------

Try:
   ./scalac-funcheck -Yshow-trees -Xprint:funcheck Test.scala

...to print the program's AST on the standard output

Try:
   ./scalac-funcheck -Ybrowse:funcheck Test.scala

...to print a Swing-based GUI for browsing the program's AST



ForAll Transformation: How does it work
-----------------------------

First, look at Test4.scala to get an idea of how we can declare properties using "our" Spec library (which has a forAll combinator)

Second, compile the whole project if you didn't yet (simply type: ant)

Third, compile the Test4.scala using scalac extended with the funcheck plugin. You can do this by typing:
    ./scalac-funcheck -cp bin:lib/ScalaCheck-1.5.jar  Test4.scala 

Now run the compiled program using standard the scala environment as follow:
    scala -cp lib/ScalaCheck-1.5.jar:. HeapTest

And you should see a similar output:

+ OK, passed 100 tests.     //Nice!! This means the property was ok!
                                                  
! Falsified after 1 passed tests.     //Good, The property was indeed wrong                                        
> ARG_0: "1"
java.lang.ExceptionInInitializerError
	[...]


Note: The ScalaCheck-1.5.jar library needs to be in the classpath for both compilation and execution because the FunCheck 
plugin rely on it for transforming every Spec.forAll (internal to our library) call to a scalacheck Prop.forAll call.