Jeck Version 0.1.0
------------------

This is the Jeck Java Finite Modeling Package 

It translates Java programs into a format which is understood by a hardcore
symbolic modeling package called Spin, which then does lots of magic.
Combined they can verify concurrency properties java program.

Directories:

docs/ - the project reports and extra documents
src/ - the Jeck Source Code
test_progs/ - test .java files used to demonstrate the translator
papers/ - referenced papers

Status: 
This was originally dreamt up for my final year project "Symbolic
Model Checking of Java" supervised by the esteemed Denis Nicole (see
enclosed report) and has only really been dabbled with since then.
Because of its intrisic dependance on the interals of an
ever-improving open source compiler Suite (KJC) most of its internals
are vastly out of date with the current running compiler version.

Anybody wishing to submit themselves to the tedium of substantially
separating this from the compiler tools, or at least setting up a
patch to a current version of the compiler, you are perfectly
welcome... although I warn you staring at hundreds of java classes
into the early hours of the morning can seriously damage your health...


Running Jeck: 
Invoke the jeck parser on a java file or files: 

$ java -classpath (insert classpath here) uk.ac.soton.ecs.jeck.Main \
   -d<ANOTDIR>  -o<OUTFILE> -t<TRANSFILE> foo.java

where

ANOTDIR: is a directory containing XML Jant (jeck annotation)
files which mark-up and override fundamentals of the java language (as
well as providing an assertion system. 

OUTFILE: is the filename for the promela output (all.prom by default) 

TRANSFILE: is the filename for the java-promela-java mapping which is
used for back-tracing. 

That should create a promela file. 

run spin on that file to create a verifier program (usually called pan) 

$ spin -J -a  -o3 all.prom
$ cc  -DVECTORSZ=4096  pan.c -o pan

Run the verifyer (and give up if it takes forever :) 

$ ./pan 

that should tell you whether or not your verification failed. 

if it did you should be able to trace through the minimium path to
failure in the java source using trans.pl in the scripts directory in
the same directory as your pan program:

$ ./trans.pl all.prom.trans all.prom.trail


simple really......


Hacking Requirements: 

KJC (www.dms.at/kopi)
---------------------
Jeck is basically a patch on the Front-end of a relatively old version
of the KJC (Kopi Java Compiler) 

You need the correct version of the KJC tree and they don't seem to 
understand CVS branches so i use the version from their CVS from
december 1999. To get it:

$ export CVSROOT=:pserver:guest@cvs.dms.at:/cvs/public
$ cvs login 
  (password is guest)
$ cvs -z3 co -D"1999/12/28 18:59:37" kopi

ANTLR
-----
KJC (used to) rely on an evilly patched version of this compiler
compiler when i made jeck, so you need to get that too (its also in
the kjc CVS repository under the antlr tree
 
$ cvs -z3 co antlr

JAVA XML Kit v1.0
-------------------
This is the original XML toolikit for java, you should be able to find
a copy of this on the java.sun.com page. 


Compiling:

Once you have everything installed  and your CLASSPATH set up. set your CLASSROOT environment
variable to where you want the compiled files to appear, then go into
the src/ directory and type make. 

this will build the files into the CLASSROOT directory in uk/ac/soton/ecs/jeck/