INSTALLATION

You can download the release of JMLForge from here. The package contains the binary package jmlforge.jar and specifications for Java API classes. To run analysis on a class you need to provide the application class path, i.e. the compiled binary code and the external library dependencies, and the source files for the application and any other relevant classes including those in Java API but missing specifications in the provided collection. The default SAT solver is SAT4J version 1.7 and it is already included in the release. If you want to use an alternative SAT solver, you need to download it from Kodkod page for your operating system.

JMLForge is able to parse the same set of JML specifications that the common JML tools support. However, it only interprets a smaller base subset of JML language and ignores other features. This also means that support for Java 1.5 generics code is currently incomplete.

LIST EXAMPLE

We are going to show you how to perform static analysis on a sample doubly-linked list implementation included in the release. The source file for jmlforge.tests.LinkList is decorated with JML specifications which model the list using an abstract field seq of type JMOObjectSequence. First, we can run analysis on get method with default settings by executing the following command:

java -jar jmlforge.jar -c jmlforge.tests.LinkList -m get

The analysis does not produce a counterexample. This may indicate that the default bounds are too low or the specification is incomplete or wrong. We can see the translation of the specification and the Java byte code into FIR by adding an option -v above which tells JMLForge to be more verbose. Alternatively, we can use option -l filename to produce an HTML log of the analysis. We can try to run the method instead of verifying the specification conformance. The following command should produce any execution of the code satisfying its specification:

java -jar jmlforge.jar -c jmlforge.tests.LinkList -m get -r

So we see that there are possible executions of the method and the specification is satisfiable. Let us try to increase the default settings. We decide to use the following bounds:

java -jar jmlforge.jar -c jmlforge.tests.LinkList -m get -w 4 -b 5 -u 2

These settings tell JMLForge to use two loop unrollings, integers in the range [-8,7], and up to five instances in each class. It is also possible to change the instance bound for any specific class using option -B. Running the analysis this time, we should luckily get a trace of a counterexample. Let us look at the trace in the log output in more detail. The root cause is highlighted in the specification statement and it is shown to be the equality constraint on the return variable. This suggests that the method returned a wrong value and we should look at the initial bindings and the arguments in the trace of the counterexample which should be similar to the following:

get_param0 = 3 get_this = jmlforge.tests.LinkList0 jmlforge.tests.LinkList$Value = [[jmlforge.tests.LinkList$Value0], [jmlforge.tests.LinkList$Value2], [jmlforge.tests.LinkList$Value3], [jmlforge.tests.LinkList$Value1], [jmlforge.tests.LinkList$Value4]] next = [[jmlforge.tests.LinkList$Value0, null], [jmlforge.tests.LinkList$Value2, jmlforge.tests.LinkList$Value3], [jmlforge.tests.LinkList$Value3, jmlforge.tests.LinkList$Value4], [jmlforge.tests.LinkList$Value1, jmlforge.tests.LinkList$Value2], [jmlforge.tests.LinkList$Value4, jmlforge.tests.LinkList$Value0]] prev = [[jmlforge.tests.LinkList$Value0, jmlforge.tests.LinkList$Value4], [jmlforge.tests.LinkList$Value2, jmlforge.tests.LinkList$Value1], [jmlforge.tests.LinkList$Value3, jmlforge.tests.LinkList$Value2], [jmlforge.tests.LinkList$Value1, null], [jmlforge.tests.LinkList$Value4, jmlforge.tests.LinkList$Value3]] seq0 = [[jmlforge.tests.LinkList0, 3, jmlforge.tests.LinkList$Value4], [jmlforge.tests.LinkList0, 0, jmlforge.tests.LinkList$Value1], [jmlforge.tests.LinkList0, 4, jmlforge.tests.LinkList$Value0], [jmlforge.tests.LinkList0, 2, jmlforge.tests.LinkList$Value3], [jmlforge.tests.LinkList0, 1, jmlforge.tests.LinkList$Value2]] size = [[jmlforge.tests.LinkList0, 5]] head = [[jmlforge.tests.LinkList0, jmlforge.tests.LinkList$Value1]] tail = [[jmlforge.tests.LinkList0, jmlforge.tests.LinkList$Value0]] ...

We see that the list contains five elements and the element at position three is jmlforge.tests.LinkList$Value4. However, in the final binding we see that the method retuns a different value:

get_return = jmlforge.tests.LinkList$Value3 get_throw = null

The returned element is located at position two in the list. If we look at the source code of the class we see that there is a bug in setting wrong terminating condition in the loop.

// if index is in back half of list, // search from the end value = tail; for (int i = size; i > index; i--) { value = value.prev; }

This condition chooses the previous element instead of the actual element in the list if the index is greater than half of the size. Therefore, the counterexample is valid and in fact pointed us to a bug in the implementation.

LINK LIST CODE & JML SPECS

//@ model import org.jmlspecs.models.*; /*@ nullable_by_default @*/ public class LinkList { //@ model instance non_null JMLObjectSequence seq; Value head, tail; int size; /*@ invariant (head == null && tail == null && size == 0) || @ (head.prev == null && tail.next == null && @ \reach(head, Value, next).int_size() == size && @ \reach(head, Value, next).has(tail) && @ (\forall Value v; \reach(head, Value, next).has(v) ; v.next != null ==> v.next.prev == v)); @*/ /*@ represents seq \such_that @ (size == seq.int_size()) && @ (head == null ==> seq.isEmpty()) && @ (head != null ==> (head == seq.get(0) && tail == seq.get(size - 1))) && @ (\forall int i ; i >= 0 && i < size - 1; ((Value)seq.get(i)).next == seq.get(i + 1)); @*/ /*@ normal_behavior @ requires index >= 0 && index < seq.int_size(); @ ensures \result == seq.get(index); @ also @ exceptional_behavior @ requires index < 0 || index >= seq.int_size(); @ signals_only IndexOutOfBoundsException; @*/ /*@ pure @*/ Value get(int index) { // check bounds if (index < 0 || index >= size ) { throw new IndexOutOfBoundsException(); } // optimize for common cases if (index == 0) return head; if (index == size - 1) return tail; Value value; // if index is in front half of list, // search from the beginning if (index <= (size >> 1)) { value = head; for (int i = 0; i < index; i++) { value = value.next; } } // if index is in back half of list, // search from the end else { value = tail; for (int i = size; i > index; i--) { value = value.prev; } } return value; } /*@ nullable_by_default @*/ public static class Value { Value next, prev; } }