Installing Java Path Finder (JPF) on Linux

[This has been written because as of now, JPF doesn't compile and work without giving you some trouble, and it took me quite some time to resolve the issues. Things might have improved at the time you read this. Also, I have tested it only on Gentoo Linux (please let me know if it breaks on a particular Linux distribution; I know there are more problems with installation on other *nix, particularly Sun Solaris)].

First things first: JPF doesn't work with Java 1.5 (aka 5.0) because of its dependence on BCEL library. If you have been able to compile successfully but can't execute JPF on simple examples (does it hang for ever?), most probably, your java version is not compatible with BCEL. Unfortunately, you will have to install an older version of JDK, perhaps 1.4.2.

Secondly, You must have JAVA_HOME variable set to your jdk root and javac should be in the PATH environment variable.

1. Checking out the source code

Create a folder where you want to download JPF. Change your working directory to that folder and type the following as a single command:

cvs -d:pserver:anonymous@cvs.sourceforge.net:/cvsroot/javapathfinder co -P javapathfinder

2. Check if you have ant installed

If you are using a new Linux distribution, most probably you already have it. Don't download in that case.

ant -version

If it displays you the version number of ant, you can read ahead. Otherwise, download and install ant first.

3. Download the "convenience libs"

JPF needs a few jars to work properly, namely BCEL, Xerces and a particular MD5 library. The JPF team has put them in a single zip (though they are older versions but they are known to work). You can download them as jpf-lib.zip from here. For convenience, move the zip file to the javapathfinder folder and unzip using the following command:

unzip jpf-lib.zip

This will create a lib folder and place the needed files there.

4. Compiling

If you now do "ant -projecthelp" from within javapathfinder folder, it will display different build options. You can build the core (without the JUnit tests) by invoking

ant compile

5. Testing out the software

(a) HelloWorld

cd examples
javac HelloWorld.java
../bin/jpf HelloWorld

It should print "Hello World!" with a thread stack trace and a "No Errors Found" message.

(b) AssertionCheck (assuming you are in the javapathfinder/examples folders)

javac AssertionCheck.java
../bin/jpf AssertionCheck

It should show you the exception trace.

6. Writing Your Own Example

If everything is working perfectly till this point, you are done. You can read the source code of the two simple examples given above. A slightly more complicated example that I tried with JPF is given below:

Suppose, we have written a findMax() function with a bug that it starts searching for the maximum value in an array starting at index 1. First, of all we have to write a "test driver" and state the properties that we expect from the code. This is given below in main(). We initialize the array with random values from Verify class.

import gov.nasa.jpf.jvm.Verify;

public class MaxWhile {
   public static int findMax (int []a) {
       int k = 1;
       int max = a[1];

       while (k < a.length) {
           if (a[k] > max) max = a[k];
           k++;
       }

       return max;
   }

   public static void main (String args[]) {
       int [] myArray = new int [Verify.random(10)];
       if (myArray.length <= 1) return;

       for (int i=0; i<myArray.length; i++)
           myArray [i] = Verify.random(10);

       int max = findMax (myArray);
       for (int i=0; i<myArray.length; i++)
           assert (max >= myArray[i]);
   }
}

Save as MaxWhile.java in examples folder. This can be compiled with javac by having gov.nasa.jpf.jvm.Verify in classpath.

javac -cp ../build/jpf MaxWhile.java
../bin/jpf MaxWhile

The code initializes an array of a random size (upper limit 10) with random values. It then finds the maximum value and checks that the maximum value obtained is indeed greater than or equal to any other value in the array. The error trace generated by JPF has Random#i at different points which collectively comprise the counterexample. They tell you different values for the random numbers that cause your assertion to fail.