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?
Lab4 - Task 3 - Aufgabe 2.4
-
- Erstie
- Beiträge: 14
- Registriert: 28. Mai 2012 19:39
-
- Kernelcompilierer
- Beiträge: 430
- Registriert: 16. Okt 2009 09:48
Re: Lab4 - Task 3 - Aufgabe 2.4
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?
-
- Erstie
- Beiträge: 14
- Registriert: 28. Mai 2012 19:39
Re: Lab4 - Task 3 - Aufgabe 2.4
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?
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?
Re: Lab4 - Task 3 - Aufgabe 2.4
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.
not via queries (pure methods)." gemacht? Das hatten wir am Anfang vergessen und hatten ähnliche Fehler.
-
- Erstie
- Beiträge: 14
- Registriert: 28. Mai 2012 19:39
Re: Lab4 - Task 3 - Aufgabe 2.4
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.
Wir haben unseren Code überprüft und greifen nur direkt über die Felder auf die Werte zu, nicht über pure - Methoden.
-
- Erstie
- Beiträge: 14
- Registriert: 28. Mai 2012 19:39
Re: Lab4 - Task 3 - Aufgabe 2.4
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.
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.
-
- Kernelcompilierer
- Beiträge: 430
- Registriert: 16. Okt 2009 09:48
Re: Lab4 - Task 3 - Aufgabe 2.4
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.