ESC/Java Validation

Document last modified: 

What is ESC/Java?

The documentation for the Compaq Extended Static Checker for Java (ESC/Java) describes itself as "a programming tool that attempts to find common run-time errors in Java programs by static analysis of the program text". 

For our purposes, validity of pre and postconditions and loop invariants can be determined statically, without executing the program code.

Use

  1. Windows:

    Download the ZIP file.

    At IUS expand to: C:\Users\your login

    The following two lines of escj.bat must be edited to the directory containing the ESCJava files and Java.exe executeable.

    set ESCJAVA_ROOT=C:\Users\your login\Escjava

    set JAVA=C:\Program Files\Java\jdk1.6.0_22\bin\java.exe

     

  2. Unix/Mac:

    Download the ZIP file.

    Set the bash shell variables to the location of where you installed ESCJava-2, if in the /Applications directory:

    export ESCTOOLS_ROOT=/Applications/ESCJava-2

    export PATH=$PATH:/Applications/ESCJava-2

  3. Validate the following insertion sort saved in file InsertionSort.java by command or shell prompt:

    escj InsertionSort.java

  4. Compile InsertionSortCall.java
     
  5. Execute by command or shell prompt:

    java InsertionSortCall

 

class InsertionSort {

//@ pre A != null;
//@ modifies A[*];
//@ post (\forall int i; 0 <= i && i < A.length-1 && A.length > 1; A[i] <= A[i+1]);

  void insertionsort(int A[]) {

        int i, j, key;

        //@ loop_invariant (\forall int k; k>=0 && k <= j-1; A[k] <= A[j-1]);

        for( j=1; j<A.length; j++) {
            key = A[j];
            i = j - 1;

           //@ loop_invariant (\forall int k; k>=0 && k < i; A[k] <= A[k+1]);

           while (i>-1 && A[i]>key) {
                 A[i+1] = A[i];
                 i = i - 1;
            }
            A[i+1] = key;
       }
   }
}

 

class InsertionSortCall {
    public static void main(String a[]) {
        int A[] = {23, 45, 12, 64, 30, 5 };
        InsertionSort is = new InsertionSort();
        is.insertionsort(A);
        
        for(int i = 0; i< A.length; i++)
            System.out.println(A[i]);
    }
}