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

Like Java, JML allows you to specify whether or not the values of a type are allowed to be null. In fact, JML makes it the default that a value of reference type is never null. In Java nullable and non_null are 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 = ...

(Note that these annotations refer to whether the reference to an object can be null, not to whether the string is empty, which sometimes is referred to as a “null string.” An empty string would be found using a non-null reference, since the string object must exist for it to be empty.)

A nullable declaration means that a variable, such as s, might be null (This must be taken into account when using that variable or verifying programs that use it.) On the other hand, a non_null declaration means that a variable, such as ss should never be null. For example, when ss is initialized or is 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. This is the default in JML; that is, if there is no modifier, a variable is assumed to be non-null.

Instead of these modifiers, one can equivalently use the Java type 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.

Here is an example. The following code

// openjml --esc T_Nullness1.java
public class T_Nullness1 {
  //@ pure
  public static boolean has(String s, char c) {
    return s.indexOf(c) != -1;
  }

  static /*@ pure 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 method has, because s is by default non-null, nor for method 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.

T_Nullness1.java:14: verify: The prover cannot establish an assertion (Precondition: T_Nullness1.java:4:) in method test
    boolean b = has(ss,'a');
                   ^
T_Nullness1.java:4: verify: Associated declaration: T_Nullness1.java:14:
  public static boolean has(String s, char c) {
                        ^
T_Nullness1.java:14: verify: Precondition conjunct is false: _JML__tmp`143 != null
    boolean b = has(ss,'a');
                    ^
T_Nullness1.java:15: verify: The prover cannot establish an assertion (Precondition: T_Nullness1.java:4:) in method test
    b = has(make(2), 'a');
           ^
T_Nullness1.java:4: verify: Associated declaration: T_Nullness1.java:15:
  public static boolean has(String s, char c) {
                        ^
T_Nullness1.java:15: verify: Precondition conjunct is false: _JML__tmp`152 != null
    b = has(make(2), 'a');
                ^
6 verification failures

Non_null and nullable as type annotations

The proper understanding of

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

is that the modifier applies 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).

As an example, consider the methods in T_Maybe shown below.

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

    //@ requires o != null;
    /*@ non_null @*/ Object fetch(/*@ nullable @*/ Object o) {
        return o;
    }

    // ensures \result <==> o == null;
    boolean isNull(/*@ nullable @*/ Object o) {
        return o == null;
    }
}

The method fetch specifies that the argument object o must not be null and simply returns it, effectively casting the argument to a non-null Object type (with JML checking that the argument is indeed non-null).

The method isNull allows its argument to be null and returns true just when it is null.

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 the String (elements) and the @Nullable goes with the array (s itself).

Nullness defaults for arrays

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 initialized. (However, one can cast array to the type @NonNull String[] once the array is full initialized if desired. For example one could write the following:

/*@ non_null @*/ String[] nna = array;

and then the array nna will be known to have all its elements be non-null. )

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 (annotations from org.jmlspecs.annotation), can be applied to either:

  • a method, in which case the given default is applicable to all types named in the method and its specification, or
  • a class, in which case the altered default applies to all types named in the class, recursively (i.e., including all types of 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.