We've decided that non-null is the default for JML (with a nuance for binary classes).
However, the elements of an array I think are a special corner case.
Typically, people write something like
Integer[] a = new Integer[10];
But that produces an array initialized to null values. One can include an initializer, if the array has fixed size (and is not too big).
But otherwise the best recourse is to initialize the array using a loop after creating it.
The problem is that the declaration above should prompt an error because by default a is an array of non-null Integers and it is not initialized that way.
Proposal: It seems to me that array elements need to be nullable no matter what the local or global default setting is.
The elements can still be explicitly declared as non-null.
We also do have \nonnullelements in JML for asserting the non-nullness of all the elements of an array.
We've decided that non-null is the default for JML (with a nuance for binary classes).
However, the elements of an array I think are a special corner case.
Typically, people write something like
But that produces an array initialized to null values. One can include an initializer, if the array has fixed size (and is not too big).
But otherwise the best recourse is to initialize the array using a loop after creating it.
The problem is that the declaration above should prompt an error because by default
ais an array of non-null Integers and it is not initialized that way.Proposal: It seems to me that array elements need to be nullable no matter what the local or global default setting is.
The elements can still be explicitly declared as non-null.
We also do have \nonnullelements in JML for asserting the non-nullness of all the elements of an array.