JML不是空变种？

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 pragma array_ != null 必须在整个程序的每个控制点保持。