NonNullModifiers

Daniel Bruns (on Feb. 14, 2014) raised the following question about non_null modifers in JML. Consider an array type. The reference manual states that when a variable of an array type is declared to be non_null, then the elements must also be non_null, recursively. The question is, whether the static type of the array or its dynamic type is used.

For example, if it means the static type, then a specification such as

//@ requires true;
public void foo (Object[][] o);

would be equivalent to the following:

/*@ requires o != null &&
  @ (\forall int i; 0 <= i && i < o.length; o[i] != null &&
  @      (\forall int j; 0 <= j && j < o[i].length; o[i][j] != null));
  @*/
public void foo (/*@ nullable @*/ Object[][] o);

It seems difficult to express a semantics that relies on the dynamic type.

Gary Leavens thinks that JML should constrain the static type of the parameters with non_null annotations, following the general principle in JML that we write specifications about static types.

David Cok suggests that we move JML to the format used in JSR 308 for type annotations, especially for array types. The advantage of this is that it would clear up this issue with more precise notation.