javaarraysnullinvariantsjml

JML not null variants?

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.

Solution

  • 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.