JML不是null变体？

Question

我有一个JML问题。它们之间的区别是什么

/*@ invariant array_ != null; */

并将其声明为

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

关于array_的元素？在每种情况下，它们的属性是什么？

提前谢谢。

Answer 1

关于array_元素的

？在每种情况下，它们的属性是什么？

对这些元素只字不提。唯一可以保证的是array_引用不为空。

注意两者之间的区别

Object[] array = null;

例如

Object[] array_ = { null };

或

Object[] array_ = { };

第一行违反了不变量，而后两行是允许的，因为array_将指向一个实际的数组(即使这个数组可能只包含空元素，甚至根本不包含元素)。

另一个不同之处在于，在invariant array_ != null;方法中，array_ != null只能在每个方法之前保持，而如果使用non_null杂注，则array_ != null必须在整个程序的每个控制点保持。