Lab4 - Task 3 - Aufgabe 2.4

[dominique.metz]

Wir schaffen es nicht, die Verträge 1 - 3 zu verifizieren.
Wir haben alle Invarianten formuliert und sie mit einem Tutor besprochen, diese sollten korrekt sein.
Auch tut die Methode add() alle Invarianten einhalten.
Nun fragen wir uns, woran es liegen könnte. add() haben wir minimal verändert (in Betrachtung von min), aber daran sollte es nicht liegen.
Kann es sein, dass der automatische Beweis hier nicht ausreicht und wir manuell den Beweis weiterführen müssen?

[Nathan Wasser]

Ich verstehe nicht welche Verträge 1 - 3 gemeint sind. Es sollen in Task 3 Aufgabe 2.4 nur die Spezifikationsfälle (i) und (ii) betrachtet werden. Hierbei sollen jeweils EnsuresPost und RespectModifies gezeigt werden. Mit welchen davon gibt es Probleme?

[dominique.metz]

Entschuldigung, natürlich meinen wir die Spezifikationsfälle 1 und 2. Sowohl EnsuresPost als auch RespectModifies für beide Fälle schlagen fehl.
Die verbleibenden "Goals" beginnen immer mit NullPointerException und ArrayIndexOutOfBoundsException. Jedoch sollte so ein Fall gar nicht auftreten, in Betracht der geltenden Invarianten und den Pre-Conditions der einzelnen Fälle.
Warum treten die Fälle trotzdem auf?

[hstr]

Habt ihr das "All elds are marked as spec public. Please access them directly in your specications and
not via queries (pure methods)." gemacht? Das hatten wir am Anfang vergessen und hatten ähnliche Fehler.

[dominique.metz]

Vielen Dank für die Antwort, doch daran liegt es leider nicht.
Wir haben unseren Code überprüft und greifen nur direkt über die Felder auf die Werte zu, nicht über pure - Methoden.

[dominique.metz]

Wir haben den Fehler gefunden.
Bei der Invariante von min haben wir die Klammerung um die "genau - dann - wenn" - Aussage vergessen. Dadurch hat die ganze Invariante natürlich keinen Sinn mehr gemacht.

[Nathan Wasser]

Für mich klingt es so als wäre in der Implementierung von add was falsch. Daher würde ich vorschlagen, dass ihr eure Implementierung nochmal anschaut, dann einen Tutor aufsucht und wenn sonst nichts hilft ihr mir die Datei schickt, denn sonst kann ich nur vage Vermutungen in den Raum stellen.