Lab 3.3.1

ratze88
Neuling
Neuling
Beiträge: 8
Registriert: 12. Sep 2013 18:30

Lab 3.3.1

Beitrag von ratze88 »

Mir ist leider irgendwie nicht so richtig klar, was in dem Problem der Aufgabe 3.1 des 3. Labs gefordert ist bzw. was ich tun soll?
Laut Aufgabenstellung soll ich die Methode ändern oder contracts hinzufügen, das ist also beides zulässig oder sogar beides zusammen nötig?
Und danach soll ich händisch in KeY durch den Beweis klicken bis ich den Beweis geschlossen habe?

Wäre super, wenn mir jemand weiterhelfen könnte. Danke!

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

Re: Lab 3.3.1

Beitrag von Nathan Wasser »

Nein, an der Methode und an den Contracts darfst Du gar nichts ändern!

Im Beweis soll man entweder durch "methodCall" Methodenaufrufe durch ihren Rumpf ersetzen (= inline methods), oder durch "Use Operation Contract" Methodenaufrufe durch ihre Spezifikation ersetzen (= make use of certain method contracts).

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

Re: Lab 3.3.1

Beitrag von Nathan Wasser »

Wichtig bei der Anwendung von Methodenaufruf-Regeln ist, dass man manchmal nur die Modalität mit dem führenden Methodenaufruf anklicken muss:
method-inlining.png
method-inlining.png (85.8 KiB) 787 mal betrachtet
und manchmal auch den Kontext dazu benötigt, also zusammen mit dem Update anklicken:
use-operation-contract.png
use-operation-contract.png (84.29 KiB) 787 mal betrachtet

Antworten

Zurück zu „Archiv“