ESC/Java Example
The original program
We provide a simple class definition, which consists of a list of numbers, and the length of this list. The methods of the class enable addition to list and sort operations.
Start by inputting the original program to ESC/Java, so you get familiar with the output of the tool. On the command prompt type:
escjava List.java
Properties of the List Class (Class Invariants)
Most of the error messages at this point mention the pointer a and the indexes for accessing it.
First, we want to point out that a can never be null. This is essential for the operations that we apply to it. ESC/Java provides the pragma non_null for checking all assignments done to a pointer are not null and assumes before each method that the pointer is not null. We add this to our class definition:
private /*@ non_null */ int a[];
When you input the new program to the tool, you will observe that the warnings of null pointer dereferencing have disappeared. Next, we can think further about our class to deal with indexing warnings.
We know that we keep N in our class because we want to keep track of how many elements are in our list. So N can never be negative nor can it exceed the length of a. This is a property of the class that does not change, i.e. it can be assumed to hold by all methods operating on the class and is required to be maintained by them. Because of it's non-changing nature, this kind of property is called a class invariant. Class invariants are expressed in ESC/Java using the pragma invariant:
/*@ invariant N >= 0 && N <= a.length */
private /*@ non_null */ int a[];
private int N;
Swap Function
We can now go on thinking about our method definitions. Let us start from the simplest, swap function.
The swap function exchanges the values stored at the positions indexed by the arguments. Therefore, we must make sure these two values make sense. In the current context this would mean that i and j are nonnegative and are less then the number of current elements stored in the list. In order to express that, our function is only guaranteed to work for these values we will add the requires pragma to the beginning of our function:
/*@ requires i >= 0 && j >= 0 && i < N && j < N */
public void swap(int i, int j) {
...
When doing its checks, ESC/Java will assume a[i] and a[j] will be indeed numbers stored in the list.
When we feed our program to the tool, we get errors that goes "Fields mentioned in this modifier pragma...", which are due to the fact that we are including some private fields of the class in our specifications. It is a good idea at this time to tell ESC/Java that we will be using both fields of the class in our specifications like any public field using the spec_public pragma:
private /*@ spec_public */ /*@ non_null */ int
a[];
private /*@ spec_public */ int N;
Now we can specify what our function does. This is done using the ensures pragma. ESC/Java checks that when the conditions in requires are met before the function runs, in the resulting state the relations in ensures holds. We expect that after the function is run, a[i] will contain the original value of a[j] and vice versa. Since in this case a[i] and a[j] both changed their values, we need the keyword old of ESC/Java to access their values before running the program. The pragma modifies is required to be able to use old, and is provided a list of a subset of the variables changed by the function. ( If a particular variable is not specified in the modifies pragma for a routine, then occurrences of that variable within arguments to old in the routine's postconditions are taken to refer to updated values)
/*@ requires i >= 0 && j >= 0 && i < N && j < N
*/
/*@ modifies a[*] */
/*@ ensures a[i] == \old(a[j]) */
/*@ ensures a[j] == \old(a[i]) */
public void swap(int i, int j) { ...
If a particular variable is not specified in the modifies pragma for a routine, then occurrences of that variable within arguments to \old in the routine's postconditions are taken to refer to updated values.
If you did not get any errors regarding the swap function, you have just verified that your function does what you expect it to.
Loop Invariants
The next function that needs to be verified it the sort function. We expect after the function is executed that the elements stored in the list will be sorted, so we note this with ensures.
/*@ ensures (\forall int i, j; (i >= 0) && (j >=
0) && (i < N) && (j < N) && (i < j) ==> a[i] <= a[j]) */
public void sortList(){...
We can further annotate the program by adding loop invariants. These comments can be said to capture the idea behind the loop. It is a property that holds before the loop, after each execution and finally when the guard doesn't hold. i.e. the loop finishes executing.
For commenting the inside of the function definition, one should consider that it is a simple implementation of the bubble sort algorithm. For the outer loop, we can say that with every execution, the smallest i elements of the list are placed at the start of the list, sorted:
/*@ loop_invariant (\forall int t,u;
(t >= 0) && (u >= 0) && (t < i) && (u < N) && (t < u) ==> a[t] <= a[u]) */
for(i = 0; i < N-1; i++) {...
For the inner loop, we can say that with every execution, the element at the ith place will be smaller than the already scanned elements, i.e. those in between i and j:
/*@ loop_invariant (\forall int u; (u >i) && (u < j) ==> a[u] >= a[i]) */
for(j = i+1; j < N; j++){...
Current commented version
The below link provides the file with the current comments. Notice that this is not claimed to be the only annotated version or to be fully commented and is probably far from that. The choice of postconditions and loop invariants are especially vast. Although one does not get major error messages from ESC/Java at this point, try running the tool with more unfolding of loops:
escjava -loop 3 List.java