JML null nicht Varianten?

Question

Ich habe eine JML Fragen. Was ist der Unterschied zwischen

/*@ invariant array_ != null; */

und erklärt es als

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

in Bezug auf die Elemente der array_? Welche Eigenschaft gilt für sie jeweils?

Vielen Dank im Voraus.

Answer 1

in Bezug auf die Elemente der array_? Welche Eigenschaft gilt für sie jeweils?

wird nichts gesagt über die Elemente. Das einzige, was garantiert ist, dass die array_ Referenz ist nicht null.

Beachten Sie den Unterschied zwischen

Object[] array = null;

und zum Beispiel

Object[] array_ = { null };

oder

Object[] array_ = { };

Die erste Zeile würde die Invariante verletzt, während die beiden letzteren erlaubt sein würde, als array_ auf eine tatsächliche Array zeigen würde (obwohl diese Anordnung nur null Elemente enthalten kann oder auch keine Elemente überhaupt).

---

Ein weiterer Unterschied besteht darin, dass in dem invariant array_ != null; Ansatz, array_ != null nur vor nach jedem Verfahren halten müssen, während, wenn Sie die non_null Pragma array_ != null nutzen an jedem Kontrollpunkt im gesamten Programm bereithalten muß.