JML 不是 null 变体？

Question

我有一个 JML 问题。 有什么区别

/*@ invariant array_ != null; */

和将其声明为

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

关于 array_ 的元素 ？在每种情况下，他们拥有什么财产？

提前致谢。

Answer 1

关于 array_ 的元素？在每种情况下，他们拥有什么属性？

没有提及有关元素的内容。唯一可以保证的是 array_ 引用不为 null。

请注意 和 之间的区别

Object[] array = null;

，例如

Object[] array_ = { null };

or

Object[] array_ = { };

第一行将违反不变量，而后两行是允许的，因为 array_ 将指向一个实际数组（即使该数组可能只包含 null 元素或甚至根本没有元素）。

---

另一个区别是，在 invariant array_ != null; 方法中，array_ != null 必须仅在每个方法之后保存，而如果您使用 non_null< /code> pragma array_ != null 必须在整个程序的每个控制点保持不变。