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.

Proving Loops with Loop Invariants

In continuation to the proof obligation posted last week, I decided to explore loop invariants. This means converting the for loop in the code to a while one. The new proof obligation is as follows:

\problem {
\<{ int[] a; int max; }\>
(
 (!a = null & a.length > 0) ->
 (
  \<{ 
   max = a[0];
   int k = 1;
   while (k < a.length) {
    if (a[k] > max) max = a[k];
    k++;
   }
  }\>
  \forall int i; (i < a.length & i >= 0 -> max >= a[i] )
 )
)
}

Now, this is much easier to prove if we can select a proper loop invariant. What is it that holds before the loop starts execution, remains true after each iteration and holds even after the loop termination? A good first attempt can be

\forall int i; (i >= 0 & i < k -> max >= a[i])

Again, the syntax is specific to KeY but the semantics are valid for any theorem prover for imperative languages. A stronger invariant can be more useful and in fact, in this particular example, the loop invariant can be strengthened to

k > 0 & k <= a.length & 
\forall int i; (i >= 0 & i < k -> max >= a[i])

There are two subcases (amongst others) generated by KeY when a loop invariant is used: Invariant Initially Valid and Body Preserves Invariant. Since we are dealing with necessity (signified by <code in angle brackets>), and not with just a possibility, we have to show termination of the loop as well. In other words, we have to show that the loop terminates and, after termination, the formula holds. Thus, the third case to prove is Termination.

Invariant Initially Valid:
 a.length >  0
==>
 \forall int i;  (i >= 0 & i <  1 -> a[0] >= a[i])


Body Preserves Invariant:
   _k >  0
 & _k <= a.length
 & \forall int i; 
     (i >= 0 & i <  _k -> _max >= a[i]),
 a.length >  0
==>
 {
   k:=_k,
   max:=_max}
   \[{method-frame(()): {
             if (k < a.length) {
                if (a[k] > max)
                   max=a[k];
                k++;
             }
       }
     }\] (\forall int i; (i >= 0 & i <  a.length -> max >= a[i])
  }

But termination is not easy to show unless we can somehow tell that something is gradually approaching towards a limit which will make the while statement false. This is where the concept of Variant is Decreasing comes in. In KeY, we can define that a.length - k is decreasing with each iteration of the loop. With the help of this statement (which of course, we have to prove separately), Termination subgoal takes the following form:

(a.length - _k) <= 0
==>
 {k:=_k,
  max:=_max}
  \<{
      while ( k < a.length ) {
         if (a[k]>max)
           max=a[k];
         k++;
      }
  }\> true

This is, of course, very easy to prove because of the premises of the implication; the loop will not execute at all and there is no statement after the loop, Hence, the termination. But while doing this, we have introduced a new sub goal: Variant is Decreasing. We have to prove that with each iteration of the loop a.length - k is actually decreasing. This subgoal has the following form:

 _k_1 >  0,
 _k_1 <= a.length,
 \forall int i;  (i >= 0 & i <  _k_1 -> _max_1 >= a[i]),
 {k:=_k_1}
   \<{method-frame(()): {
         var=k       }
     }\> var = TRUE,
 a.length >  0
==>
 {k:=_k_1,
   max:=_max_1,
   var_1:=a.length - _k_1}
   \<{
        if (a[k]>max)
          max=a[k];
        k++;
     }\> (a.length - k) <  var_1

It looks daunting but after symbolic execution of the code, it's pretty simple.

Once we have proved everything regarding the invariant, we can use the invariant to prove the real thing, which was the following first order logical formula:

\forall int i; (i < a.length & i >= 0 -> max >= a[i] )

Thus, the fourth case, called Use Case is something of the form

k > 0 & k <= a.length & 
\forall int i; (i >= 0 & i < k -> max >= a[i]) ==>
\forall int i; (i < a.length & i >= 0 -> max >= a[i] )

which is much easier to prove than the standalone formula that we initially had.

---

My affair with loop invariants was a very short one. Perhaps, I'll come back to these in future. At present, I'm moving on to manually injecting bugs in this code and trying to find them using KeY.

First Steps in Theorem Proving using KeY

Now something very technical! I'll try to keep it simple; as simple as possible, but not any simpler.

Following is a .key file that has Java code in between \<{ and }\>. The code looks for the maximum element in the array. The first order logical formula (after the block of code) says that when the code has been executed, the variable max will hold a value greater than or equal to every element of the array.

\problem {
\<{ int[] a; int max; }\>
(
 (!a = null & a.length > 0) ->
 (
  \<{ 
   max = a[0];
   for (int i=0; i<a.length; i++) {
    if (a[i] > max) max = a[i];
   }
  }\>
  \forall int i; (i < a.length & i >= 0 -> max >= a[i] )
 )
)
}

This format is internal to the KeY tool. But the ideas will be similar to any theorem prover for imperative programming languages, like Java.

At the moment, I am stuck up because there is no upper limit on the size of the array, which tells me that the only way to prove the formula is to use induction. Now, the only sequence that can be made a basis for induction is the size of the array. I'm trying to figure out how to state this in KeY.

Technical Humor

A function and a differentiation operator meet somewhere in Hilbert space.

The differentiation operator: Make place or I differentiate you.

Function: Forget it buster, I am e^x.

The differentiation operator: Well, I am d/dy.

(More like these)