Whether references to objects are null or not is a highly important property in Java programs and just about every other programming language, to the point that some languages are including non-nullness as a property of the type of a variable.

JML also allows you to specify whether or not something is allowed to be null. In fact, JML makes it the default that a value of reference type is never null. Furthermore, Java has introduced type annotations (since Java 8), which are annotations on types rather than on declarations. The switch to type annotations for nullness changes the syntax of JML in ways that might be surprising or at least unfamiliar to long-time JML users.

Simple uses of non-null and nullable

At the simplest level, declarations of a variable may include the modifiers non_null or nullable:

/*@ nullable */ String s = ...
/*@ non_null */ String ss = ...

These declarations mean that wherever s is used, it must be taken into account that s might be null. On the other hand, ss is specified to never be null. Accordingly, when ss is initialized or the target of an assignment, the value it is given must be provably not null. But thereafter the values can be assumed to be non-null. If there is no modifier, the default is non-null.

Instead of these modifiers, one can use the Java annotations @NonNull or @Nullable (if one imports the package org.jmlspecs.annotation).

The above modifiers are applicable to local declarations, field declarations, formal parameter declarations, and method return type declarations.

! Caveat: the default for local declarations is still under discussion. OpenJML uses the same default as for types in other places.

Here is an example. The code

// openjml --esc T_Nullness1.java
public class T_Nullness1 {

  public static boolean has(String s, char c) {
    return s.indexOf(c) != -1;
  }

  static /*@ nullable */ String make(int i) {
    if (i<0) return null;
    return String.valueOf(new char[i]);
  }

  public static void test(/*@ nullable */ String ss) {
    boolean b = has(ss,'a');
    b = has(make(2), 'a');
  }
}

produces no errors for has because s is by default non-null, nor for make, because the return value of make is allowed to be null. But it does issue verification errors for both statements in test because both ss and the result of make may be null and the argument of has is not allowed to be null.

Non_null and nullable as type annotations

The proper understanding of

/*@ non_null */ String ss = ...

is that the modifier appplies to the type String, not to ss directly. That is ss has type @NonNull String. In fact, as a type annotation, non_null can be applied to any use of the type: along with the declarations mentioned above, that includes type names in cast expressions, in instanceof expressions, in type parameters, even as a modifier of a type variable — in short, anywhere a type name is allowed, it may be modified with a type annotation. However, type annotations on types in the extends and implements clauses of a class declaration are meaningless and ignored (except on generic type arguments).

TODO - more examples here

Type annotations and fully-qualified type names

Java’s syntax for type annotations applied to fully-qualified type names is a bit unexpected. One writes java.lang.@NonNull String (rather than the incorrect @NonNull java.lang.String).

Type annotations and arrays

Applying annotations to arrays also requires some peculiar Java syntax. The difficulty is that one must distinguish between non-null array references and non-null array elements. Java stipulates that

@NonNull String @Nullable [] s;

declares s to have the type possibly null array of non-null String values. That is the @NonNull (or equivalently /*@ non_null */) goes with String and the @Nullable goes with the array.

Nullness defaults for arrays

! Caveat: the nullness default for array elements is still under discussion

While non-null is the overall default, that causes a problem for arrays. The standard way to create and initialize an array is this:

String[] array = new String[100];
for (int i = 0; i < array.length; i++) array[i] = ...

But the constructor for a new array, new String[100], creates an array with null elements. So the type of array cannot be @NonNull String[], even if we would like that to be the type once it is fully intialized.

TODO - more needs to be said here

Changing the default

As stated above, JML applies a default non_null modifier where no non_null or nullable indication is otherwise given. This default can be changed. The modifiers non_null_by_default or nullable_by_default, or their equivalents @NonNullByDefault and @NullableByDefault, can be applied to

  • a method, in which case the given default is applicable to all types named in the method and its specification
  • a class, in which case the altered default applies to all types named in the class, recursively (fields and methods and nested classes)

In addition, tools may provide ways to set the global default. OpenJML has command-line options --nonnull-by-default and --nullable-by-default that set the default for all the files being analyzed. It is generally preferable to use explicit defaults at the class or method level, because using global tool options may affect files (like library specification files) that are expecting the normal non-null default to apply.

For example,

// openjml --esc T_NullnessDefault.java
//@ non_null_by_default
public class T_NullnessDefault {

  public void test(String s) {
    int h = s.hashCode();
  }
}

verifies because s is a @NonNull String so the dereference in s.hashCode is OK. But the code

// openjml --esc T_NullnessDefault2.java
//@ nullable_by_default
public class T_NullnessDefault2 {

  public void test(String s) {
    int h = s.hashCode();
  }
}

produces a verification error

T_NullnessDefault2.java:6: verify: The prover cannot establish an assertion (PossiblyNullDeReference) in method test
    int h = s.hashCode();
             ^
1 verification failure

because at the dereference of s it cannot be proven that s is non-null, because the default for the type in the formal parameter declaration is now nullable.