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_;
regardi开发者_运维百科ng the elements of array_? What property holds for them in each case?
Thanks in advance.
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.
精彩评论