nullness default for arrays

[davidcok]

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.

[leavens]

The suggestion of making the default for array elements be nullable seems sensible to me. I only wonder if we should think about a non-null default for array arguments. However, that would lead to additional complications, so this proposal is okay with me.

[mattulbrich]

I do not think that it is necessary to have a shallow nonnull since local variables are nullable by default. I do not see where the shallow non-null is really needed.

[davidcok]

Local variables have the same default as fields -- generally non null,-- or so I thought. It seems to me pretty crucial for usability to have the default for array elements be nullable -- shallow as Mattias puts it. So I'm not following your thinking Mattias.

[mattulbrich]

The reference manual says:

6.2.13 Nullity Modifiers

Any declaration (other than that of a local variable) whose type is a reference type is implicitly declared non_null unless (explicitly or implicitly) declared nullable.

It would be quite a change, changing the semantics of nonull. I by now followed the reasoning behind deep non_null that Patrice Chalin one found out.

[davidcok]

OK. I did not realize that the DRM said that. And would not have agreed with it if I had. I really don't like the default for local variables being different than for fields.

But for array elements, the standard idiom of Object[] o = new Object[10]; ... initialize the elements

whether o is a field or local just can't be specified if the array elements are non null by default.