JML: "ensures" und "assignable \nothing"

dominik.reis
Neuling
Neuling
Beiträge: 4
Registriert: 5. Dez 2011 21:06

JML: "ensures" und "assignable \nothing"

Beitrag von dominik.reis »

Hallo,

ich habe mal ein Frage zu Problem 5 aus Exercise 4.

In der Lösung zur add-Methode steht folgender Contract:

Code: Alles auswählen

    /*@ public normal_behavior
      @ ...
      @
      @ also
      @
      @ public normal_behavior
      @ requires (size == limit) || contains(elem);
      @ ensures \result == false; 
      @ ensures (\forall int e; contains(e) <==> \old(contains(e)));
      @ ensures size == \old(size);
      @ assignable \nothing;
      @*/
Für mich stellt sich nun die Frage, ob die folgenden beiden ensures überhaupt notwendig sind, da assignable \nothing doch bereits dafür sorgt, dass arr als auch size unverändert bleibt?

Code: Alles auswählen

      @ ensures (\forall int e; contains(e) <==> \old(contains(e)));
      @ ensures size == \old(size);

Nathan Wasser
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: JML: "ensures" und "assignable \nothing"

Beitrag von Nathan Wasser »

Korrekt erkannt.

Sie sind nicht falsch, aber durch das "assignable \nothing;" sind sie nicht nötig.

dominik.reis
Neuling
Neuling
Beiträge: 4
Registriert: 5. Dez 2011 21:06

Re: JML: "ensures" und "assignable \nothing"

Beitrag von dominik.reis »

Alles klar.
Danke für die Antwort!

Antworten

Zurück zu „Archiv“