2

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.

trnc
  • 20,581
  • 21
  • 60
  • 98

1 Answers1

2

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.

aioobe
  • 413,195
  • 112
  • 811
  • 826