JML NOT NULL varianti?

Question

ho un domande JML. qual è la differenza tra il

/*@ invariant array_ != null; */

e dichiarando come

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

per quanto riguarda gli elementi di array_? Quali proprietà vale per loro in ogni caso?

Grazie in anticipo.

Answer 1

  

per quanto riguarda gli elementi di array_? Quali proprietà vale per loro in ogni caso?

Nulla è detto circa gli elementi. L'unica cosa che è garantito è che il riferimento array_ non è nullo.

Si noti la differenza tra

Object[] array = null;

e, per esempio

Object[] array_ = { null };

o

Object[] array_ = { };

La prima linea violerebbe l'invariante, mentre gli ultimi due sarebbe consentito, come array_ indicherebbe una matrice reale (anche se questa matrice può contenere solo elementi nulli o addirittura nessun elementi affatto).

---

Un'altra differenza è che nell'approccio invariant array_ != null;, array_ != null deve contenere solo prima dopo ogni metodo, mentre se si utilizza il non_null array_ != null pragma deve valere in ogni punto di controllo in tutto il programma.