относительно элементов array_? Какое свойство имеет для них в каждом случае?
Ничего не сказано об элементах. Гарантируется только то, что ссылка array_ не равна нулю.
Обратите внимание на разницу между
Object[] array = null;
и, например,
Object[] array_ = { null };
или
Object[] array_ = { };
Первая строка будет нарушать инвариант, в то время как последние две будут разрешены, поскольку array_ будет указывать на фактический массив (даже если этот массив может содержать только нулевые элементы или даже вообще не содержать элементов).
Другое отличие состоит в том, что в подходе invariant array_ != null; array_ != null должен удерживаться только после каждого метода, в то время как при использовании non_null прагма array_ != null должна удерживаться в каждой контрольной точке всей программы.