Introduction
JACK is a prototype tool for checking Java annotations. Currently, it supports only @NonNull annotations, although we plan to extend this to others (e.g. @ReadOnly, @Secure) in the future. The tool uses type inference technology (specifically, flow-sensitive dataflow analysis) in order to infer the affect of conditional statements on variable types. The tool assumes method parameters, return types and fields are already annotated appropriately. With this information, it checks method bodies for "type errors". For example, consider the following program:
public class Example {
String aField;
public void set(String f) { aField = f; }
public String toString() {
return aField.toString();
}}
We consider this program to contain a bug. This arises then the toString() method is called when aField is null. JACK reports the following errors for this program:
> jack Example.java
Type error: method toString : String (@NonNull Example)
not subtype of @NonNull String (@NonNull Object)
Type error: method invocation not permitted on type (Example.java:7)
The first error indicates that the toString method must return a @NonNull value. The second says that we can't invoke a method on a value which is not known to be @NonNull. Now, we can try and fix this by adding @NonNull annotations appropriately:
import jack.types.*;
public class Example {
@NonNull String aField;
public void set(@NonNull String f) { aField = f; }
public @NonNull String toString() {
return aField.toString();
}}
Here, we have used the @NonNull annotation to state that aField can never hold the null value. Likewise we must also annotate the parameter for set, otherwise jack would report an error. This time, running jack gives the following:
> jack Example.java Type error: field "aField" not properly initialised (Example.java:3)This tells us that we forgot something --- the field is initialised by default to
null! Since this would break the @NonNull invariant, we must provide a proper initialisation value like so:
import jack.types.*;
public class Example {
@NonNull String aField = "";
public void set(@NonNull String f) { aField = f; }
public @NonNull String toString() {
return aField.toString();
}}
This time, jack will compile the code without error.
Download
| Release | Date | Arch | Files | Notes |
| 0.3 (ALPHA) | October 2007 | UNIX (inc. Linux) / Cygwin | jack-v0.3-alpha.tgz |  |
| 0.2 (ALPHA) | January 2007 | UNIX (inc. Linux) / Cygwin | jack-v0.2-alpha.tgz | |
| 0.1 (ALPHA) | December 2006 | UNIX (inc. Linux) / Cygwin | jack-v0.1-alpha.tgz | |