JML no es nulo variantes?
-
08-10-2019 - |
Pregunta
Tengo un JML preguntas. ¿cuál es la diferencia entre
/*@ invariant array_ != null; */
y declarando como
protected /*@ non_null */ Object[] array_;
con respecto a los elementos de array_? Lo que la propiedad vale para ellos en cada caso?
Gracias de antemano.
Solución
con respecto a los elementos de array_? Lo que la propiedad vale para ellos en cada caso?
No se dice nada acerca de los elementos. Lo único que está garantizado es que la referencia array_
no es nulo.
Tenga en cuenta la diferencia entre
Object[] array = null;
y, por ejemplo
Object[] array_ = { null };
o
Object[] array_ = { };
La primera línea violaría la invariante, mientras que los dos últimos se permitiría, como array_
apuntaría a una matriz real (a pesar de que esta matriz única puede contener elementos nulos o incluso no hay elementos en absoluto).
Otra diferencia es que en el enfoque invariant array_ != null;
, array_ != null
sólo debe contener antes después de cada método, mientras que si se utiliza el non_null
array_ != null
pragma debe ser titular en todos los puntos de control a lo largo del programa.