JML не нулевые варианты?

Question

JML не нулевые варианты?

У меня есть вопросы JML. в чем разница между

/*@ invariant array_ != null; */

и объявив его как

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

относительно элементов array_? Какое свойство имеет для них в каждом случае?

Заранее спасибо.

2

java arrays null invariants jml

Источник

user193643 05 дек '10 в 15:10

1 ответ

Решение

Другие вопросы по тегам java arrays null invariants jml

user276052 05 дек '10 в 15:12 2010-12-05 15:12 · Accepted Answer · 2010-12-05 15:12

относительно элементов array_? Какое свойство имеет для них в каждом случае?

Ничего не сказано об элементах. Единственное, что гарантировано, это то, что array_ ссылка не является нулевой.

Обратите внимание на разницу между

Object[] array = null;

и например

Object[] array_ = { null };

или же

Object[] array_ = { };

Первая строка будет нарушать инвариант, в то время как последние два будут допущены, так как array_ будет указывать на фактический массив (даже если этот массив может содержать только нулевые элементы или вообще не содержать элементов).

Другое отличие состоит в том, что в invariant array_ != null; подход, array_ != null должен удерживаться только после каждого метода, а если вы используете non_null прагма array_ != null должен удерживаться в каждой контрольной точке на протяжении всей программы.