JML not null variants?

Question

i have a JML questions. what is the difference between

/*@ invariant array_ != null; */

and declaring it as

protected /*@ non_null */ Object[] array_;

regarding the elements of array_? What property holds for them in each case?

Thanks in advance.

Answer 1

regarding the elements of array_? What property holds for them in each case?

Nothing is said about the elements. The only thing that is guaranteed is that the array_ reference is not null.

Note the difference between

Object[] array = null;

and for instance

Object[] array_ = { null };

or

Object[] array_ = { };

The first line would violate the invariant, while the latter two would be allowed, as array_ would point to an actual array (even though this array may only contain null elements or even no elements at all).

---

Another difference is that in the invariant array_ != null; approach, array_ != null must only hold before after each method, while if you use the non_null pragma array_ != null must hold at every control point throughout the program.