JMLはnullではありませんか？

Question

私はJMLの質問があります。 array_の要素に関する

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

として、それを宣言する

/*@ invariant array_ != null; */ 

との違いは何ですか？それぞれの場合、どのような財産がありますか？

ありがとうございます。

Answer 1

array_の要素については？それぞれの場合、どのような財産がありますか？

要素については何も言及されていません。保証されているのは、array_の参照がnullでないことだけです。

注

Object[] array = null; 

間、例えば差

Object[] array_ = { null }; 

又は

Object[] array_ = { }; 

後者の二つは許されるであろうしながら最初の行は、不変量に違反する、などarray_は、実際の配列を指しています（ただし、この配列はcontヌル要素、または全く要素がない場合もあります）。

---

もう1つの違いは、あなたがnon_nullプラグマを使用する場合array_ != nullは、プログラム全体のすべての制御ポイントで保持しなければならないがinvariant array_ != null;アプローチでは、array_ != nullのみ、各メソッドの後の前に保持しなければならないということです。