Si comunicado con el regreso de JML

Question

i necesidad de establecer un postcondition que asegura a nulo retorno si size_ es 0. Basado en

 if(size_ == 0)
  return null;

¿Cómo puedo hacer que en JML? ¿algunas ideas? Siguiente no funciona:

//@ ensures size_ == null ==> \return true;

gracias de antemano

Answer 1

Trate

//@ ensures size_ == null ==> \result == true;

Ejemplo:

//@ ensures size_ == null ==> \result == true;
public boolean sizeUndefined() {
    if (size_ == null)
        return true;

    return size_.length() > 0;
}

También podría simplemente escribir así:

//@ ensures size_ == null ==> \result;

Aquí es la documentación para \result :

3.2.14 \result
Dentro de un postcondition normal o un objetivo de la modificación de un método no vacío, el identificador especial \ resultado es una expresión especificación cuyo tipo es el tipo de retorno del método. Denota el valor devuelto por el método. \ Resultado sólo se permite dentro de un pragma se cerciora, also_ensures, modifica o also_modifies que modifica la declaración de un método no nula.

Answer 2

En primer lugar: ¿qué tipo es size_, Object o primitive(int)

En segundo lugar, lo que el tipo de retorno del método? Object o primitive(boolean)?

No se puede comparar un tipo primitivo de null o null retorno donde se supone que un tipo primitivo que ser devuelto. Si asumimos size_ es int y el retorno es boolean entonces el post-condición sería

//@ ensures size_ == 0 ==> \result;