If-Anweisung mit Rückkehr in JML

Question

Ich brauche eine Nachbedingung einzurichten, die sicher auf null zurück, wenn size_ 0. Basierend auf

 if(size_ == 0)
  return null;

Wie kann ich tun, dass in JML? irgendwelche Ideen? Im Anschluss funktioniert nicht:

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

Vielen Dank im Voraus

Answer 1

Versuchen

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

Beispiel:

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

    return size_.length() > 0;
}

Sie können auch einfach schreiben Sie es wie folgt aus:

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

Hier ist die Dokumentation für \result :

3.2.14 \result
Innerhalb eines normalen Nachbedingung oder einer Modifikation eines Ziel-nicht-Void-Methode, die spezielle Kennung \ Ergebnis ist ein Ausdruck, dessen Typ-Spezifikation ist der Rückgabetyp der Methode. Es bezeichnet den Wert, der durch das Verfahren zurückgeführt. \ Ergebnis darf nur innerhalb eines sichert also_ensures, ändert oder also_modifies pragma dass ändert die Erklärung eines nicht-Void-Methode.

Answer 2

Zu allererst: welche Art ist size_, Object oder primitive(int)

Zweitens, was der Rückgabetyp der Methode? Object oder primitive(boolean)?

Sie können keine primitive Art zu null oder Rückkehr null vergleichen, wo ein primitiver Typ soll zurückgegeben werden. Wenn wir davon ausgehen, size_ ist int und die Rückkehr ist boolean dann die der Post-Zustand wäre

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