Lab4 - Task 3 - Aufgabe 2.4

dominique.metz
Erstie
Erstie
Beiträge: 14
Registriert: 28. Mai 2012 19:39

Lab4 - Task 3 - Aufgabe 2.4

Beitrag von 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
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: Lab4 - Task 3 - Aufgabe 2.4

Beitrag von 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
Erstie
Erstie
Beiträge: 14
Registriert: 28. Mai 2012 19:39

Re: Lab4 - Task 3 - Aufgabe 2.4

Beitrag von 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
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 128
Registriert: 14. Apr 2011 22:52

Re: Lab4 - Task 3 - Aufgabe 2.4

Beitrag von 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
Erstie
Erstie
Beiträge: 14
Registriert: 28. Mai 2012 19:39

Re: Lab4 - Task 3 - Aufgabe 2.4

Beitrag von 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
Erstie
Erstie
Beiträge: 14
Registriert: 28. Mai 2012 19:39

Re: Lab4 - Task 3 - Aufgabe 2.4

Beitrag von 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
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: Lab4 - Task 3 - Aufgabe 2.4

Beitrag von 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.

Antworten

Zurück zu „Archiv“