JML について質問があります。違いは何ですか
/*@ invariant array_ != null; */
そしてそれを次のように宣言します
protected /*@ non_null */ Object[] array_;
array_?の要素について それぞれの場合にどのようなプロパティが保持されますか?
前もって感謝します。
質問する
1139 次
1 に答える
2
array_?の要素について それぞれの場合にどのようなプロパティが保持されますか?
要素については何も言われていません。保証されている唯一のことは、array_参照が null でないことです。
の違いに注意してください
Object[] array = null;
そして例えば
Object[] array_ = { null };
また
Object[] array_ = { };
最初の行は不変条件に違反しますが、後の 2 行はarray_実際の配列を指すため、許容されます (この配列には null 要素しか含まれていないか、要素がまったく含まれていない可能性があります)。
もう 1 つの違いは、このinvariant array_ != null;アプローチでは各メソッドの前にのみ保持する必要があるのに対し、プラグマarray_ != nullを使用する場合はプログラム全体のすべての制御点で保持する必要があることです。non_nullarray_ != null
于 2010-12-05T15:12:47.770 に答える