JML不爲null變體？

Question

我有一個JML問題。正是因爲

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

關於array_的元素

/*@ invariant array_ != null; */ 

，並宣佈它的區別？每種情況下他們擁有哪些財產？

在此先感謝。

Answer 1

關於array_的元素？每種情況下他們擁有哪些財產？

沒有關於元素的說法。唯一保證的是array_引用不爲空。

注

Object[] array = null; 

之間並且例如差

Object[] array_ = { null }; 

或

Object[] array_ = { }; 

第一行會違反不變的，而後者2將被允許，因爲array_會指向一個實際的數組（即使這個數組可能只有連續ain null元素甚至根本沒有元素）。

---

另一個不同之處是，在invariant array_ != null;方法，array_ != null只能每種方法後舉行之前，而如果你使用non_null編譯array_ != null必須在整個程序中的每個控制點舉行。