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

ReleaseDateArchFilesNotes
0.3 (ALPHA) October 2007 UNIX (inc. Linux) / Cygwin jack-v0.3-alpha.tgz book icon
0.2 (ALPHA) January 2007 UNIX (inc. Linux) / Cygwin jack-v0.2-alpha.tgz book icon
0.1 (ALPHA) December 2006 UNIX (inc. Linux) / Cygwin jack-v0.1-alpha.tgz book icon

Documentation

Not yet! Please read the README file included in the distribution.