An illustrative example of using ESC/Java

To give the reader a general idea of what ESC/Java does and how to use it, we begin with an example illustrating some salient features of ESC/Java through its application to a simple class declaration deliberately seeded with some errors.

Scene 0:  We write a class declaration.

Our example is the class Bag declared in a file Bag.java as follows:
line
 1:  class Bag {
 2:    int[] a;
 3:    int n;
 4:
 5:    Bag(int[] input) {
 6:      n = input.length;
 7:      a = new int[n];
 8:      System.arraycopy(input, 0, a, 0, n);
 9:    }
10:
11:    int extractMin() {
12:      int m = Integer.MAX_VALUE;
13:      int mindex = 0;
14:      for (int i = 1; i <= n; i++) {
15:        if (a[i] < m) {
16:          mindex = i;
17:          m = a[i];
18:        }
19:      }
20:      n--;
21:      a[mindex] = a[n];
22:      return m;
23:    }
24:  }
A copy of this program is in escjavaRoot/examples/0.0/Bag.java, where escjavaRoot denotes the (site-specific) top-level directory for ESC/Java (see appendix B).  The idea is that an object x of class Bag represents a multiset (also known as a ``bag'') of integers in the form of integer array x.a together with an integer x.n, where the elements of the multiset are the first x.n elements of the array.  In our example declaration, we define a constructor that creates a Bag from an array, and a single method extractMin that finds, removes, and returns the minimal element of a Bag. The extractMin method iterates over the first this.n elements of this.a, keeping track of the smallest one in the local variable m .  After finding the smallest element of this.a,  it copies the element at the highest used position of x.a into the position formerly occupied by the minimum element, decreases the count of used elements, and returns the value that was saved in m .

Scene 1:  We run ESC/Java, and it warns of two potential null dereferences.

To compile Bag.java, we would type the command line:
javac Bag.java
To check our definition of class Bag with ESC/Java, we instead type the following similar command line:
escjava Bag.java
ESC/Java then produces the following output:
Bag.java:6: Warning: Possible null dereference (Null)
    n = input.length;
             ^
Bag.java:15: Warning: Possible null dereference (Null)
      if (a[i] < m) {
           ^
Execution trace information:
    Completed 0 loop iterations in "Bag.java", line 14, col 4.

Bag.java:15: Warning: Array index possibly too large (IndexTooBig)
      if (a[i] < m) {
           ^
Execution trace information:
    Completed 0 loop iterations in "Bag.java", line 14, col 4.

Bag.java:21: Warning: Possible null dereference (Null)
    a[mindex] = a[n];
                 ^
Execution trace information:
    Completed 0 loop iterations in "Bag.java", line 14, col 4.

Bag.java:21: Warning: Possible negative array index (IndexNegative)
    a[mindex] = a[n];
                 ^
Execution trace information:
    Completed 0 loop iterations in "Bag.java", line 14, col 4.

5 warnings

Remark:  Actually,  the above is the output generated by the command

escjava -quiet Bag.java
The normal output of ESC/Java also includes various progress messages and timing information which are omitted here.

Remark:  Some of the messages above include a part marked as ``Execution trace information''.  We say more about execution traces below, particularly in section 4.0, but will not discuss them further in the course of this introductory example.

Scene 2:  We write a requires (precondition) pragma for the Bag constructor.

ESC/Java's first warning is that the attempt on line 6 to access input.length might fail because input might be null.  We now must decide what to do about this warning.

One approach would be to decide that the implementation of the constructor is incorrect.  Following this approach, we would modify the constructor to test for a null argument and, for example, construct an empty multiset:

  Bag(int[] input) {
    if (input == null) {
      n = 0;
      a = new int[0];
    } else {
      n = input.length;
      a = new int[n];
      System.arraycopy(input, 0, a, 0, n);
    }
  }
This would indeed eliminate the first warning.  Instead, however, we will continue our example by illustrating a second approach, in which we decide that the implementation of the constructor is correct, but that we do not intend for the constructor ever to be called with a null argument.  We inform ESC/Java of this decision by adding an annotation to the constructor declaration:
       //@ requires input != null;
       Bag(int[] input) {
         n = input.length;
       ...
When the character @ is the first character after the initial // or /* of a Java comment, as in the first line of the program fragment above, ESC/Java expects the body of the comment to consist of a sequence of ESC/Java annotations, known as pragmas.  The requires pragma above specifies a precondition for the constructor, that is, a boolean expression which must be true at the start of any call.  When checking the body of a method or constructor that is annotated with a precondition, ESC/Java can assume the truth of the precondition to confirm the absence of errors in the body (for example, the absence of a null dereference during the evaluation of input.length in the code fragment above).  When checking code that calls a method or constructor annotated with a precondition, ESC/Java will issue a warning if it cannot confirm that the precondition (with the values of the actual parameters substituted for the formal parameter names) would always evaluate to true at the call site.

Scene 3:  We add a non_null pragma for the field a.

So much for the first warning.  We now turn our attention to the second warning:
Bag.java:15: Warning: Possible null dereference (Null)
      if (a[i] < m) {
           ^
Here, ESC/Java is warning that the array variable a (actually this.a) might be null.  We could deal with this warning by either of the approaches discussed above in connection with the first warning--that is, by adding the precondition requires a != null to the extractMin method, or by adding special code for the case a == null. However ESC/Java offers yet another choice, which is to specify that the a field of any Bag is always supposed to be non-null.  To do this, we annotate the declaration of a with a non_null pragma:
     class Bag {
       /*@ non_null */ int[] a;
       ...
This causes ESC/Java to assume that the a field of any Bag object is itself non-null (and thus can safely be dereferenced).  Conversely, it causes ESC/Java to issue a warning for any assignment to the a field of a Bag, if it cannot confirm that the expression being assigned will have a non-null value at run time.  Furthermore ESC/Java will check that every Bag constructor initializes the a field of the constructed object to a non-null value.

Scene 4:  We correct a bug in Bag.extractMin.

We now consider the third warning:
Bag.java:15: Warning: Array index possibly too large (IndexTooBig)
      if (a[i] < m) {
           ^
Examining the program, we now find a genuine bug.  The for loop starting on line 15 (in the original program) examines array elements a[1] through a[n], but array indexing in Java is zero based.  We correct the line to read
        for (int i = 0; i < n; i++) {

Scene 5:  We take no action for a redundant warning.

The fourth warning
Bag.java:21: Warning: Possible null dereference (Null)
    a[mindex] = a[n];
                 ^
requires no action, as the non_null pragma we added in section 0.3 already prevents a from being null.  In other words, the second and fourth warnings complain about the same problem.
Remark:  ESC/Java often avoids issuing such redundant warnings.  Note, for example, that it doesn't complain about the expression a[m] on (original) line 17, or the expression a[mindex] on the left hand side of the assignment on (original) line 21.  However, it does not avoid them in all cases.  A detailed description of the circumstances in which ESC/Java will or will not issue multiple warnings with the same underlying cause is beyond the scope of this manual.

Scene 6:  We supply a precondition for Bag.extractMin.

We now consider the last of the five warnings:
Bag.java:21: Warning: Possible negative array index (IndexNegative)
    a[mindex] = a[n];
                 ^
The problem is that the code in (original) lines 20-21 removes an element from the bag even when the bag is already empty (that is, when this.n == 0 on entry to extractMin).  ESC/Java has called our attention to the need for another design decision:  do we add special code to handle the situation when extractMin is called on an empty bag, or do we add a precondition forbidding such calls?  Let's try the latter course:
12:    //@ requires n >= 1;
13:    int extractMin() {

Scene 7:  We run ESC/Java again and it still issues a warning.

With all the changes described above, our example program now reads:
 1:  class Bag {
 2:    /*@ non_null */ int[] a;
 3:    int n;
 4:
 5:    //@ requires input != null;
 6:    Bag(int[] input) {
 7:      n = input.length;
 8:      a = new int[n];
 9:      System.arraycopy(input, 0, a, 0, n);
10     }
11:
12:    //@ requires n >= 1;
12:    int extractMin() {
13:      int m = Integer.MAX_VALUE;
14:      int mindex = 0;
15:      for (int i = 0; i < n; i++) {
16:        if (a[i] < m) {
17:          mindex = i;
18:          m = a[i];
19:        }
20:      }
21:      n--;
22:      a[mindex] = a[n];
23:      return m;
24:    }
25:  }
We now run ESC/Java again and it produces the following warning:
Bag.java:17: Warning: Array index possibly too large (IndexTooBig)
      if (a[i] < m) {
           ^

Scene 8:  We supply an invariant pragma relating n to a.lenght.

It may appear that ESC/Java is still complaining about the bug we thought we'd fixed in section 0.4, but further study reveals a different problem:  ESC/Java has no reason to expect that n, which we intend to be the length of the meaningful prefix of a, will in fact be at most a.length.   We can express this intention with an invariant pragma:
 1:  class Bag {
 2:    /*@ non_null */ int[] a;
 3:    int n;
 4:    //@ invariant 0 <= n & n <= a.lenght;
...
Roughly speaking, ESC/Java treats an invariant as an implicit postcondition of every constructor and as both a precondition and postcondition of every method.  The semantics of invariant pragmas--and all other ESC/Java pragmas--are described in greater detail in section 2 below.  The full rules about expressions that can occur in pragmas (called specification expressions) are given in section 3.  For now, we remark that since specification expressions are not actually executed, the unconditional logical operators & and | are interchangeable (except for binding power) in specification expressions with the respective conditional operators && and ||.

Scene 9:  ESC/Java notices a typographical error.

When we run ESC/Java again, the result is:
Bag.java:4: Error: No such field in type int[]
  //@ invariant 0 <= n & n <= a.lenght;
                                ^
Caution: Turning off extended static checking due to type error(s)
1 caution
1 error

Scene 10:  Our efforts come to a happy conclusion.

Whoops!  Our invariant pragma had a spelling error. We correct it to read
 4:    //@ invariant 0 <= n & n <= a.length;
and try again.  This time ESC/Java runs without reporting any further complaints.

The file escjavaRoot/examples/0.10/Bag.java contains a copy of the final version of the Bag class.