Seite 1 von 1

Lab4 Invarianten

Verfasst: 20. Feb 2013 17:44
von khaled
Hallo,
Kann mir jemanden sagen wie ich die Invarianten ( in Task3.1 ) in KeY verifizieren kann.

Khalid

Re: Lab4 Invarianten

Verfasst: 20. Feb 2013 17:58
von mmi1991
Wie willst du Invarianten "direkt" beweisen?
Bei Task 3.1. sehe ich nichts von JML Invarianten beweisen.

Invarianten *sollen* immer gelten. Somit kannst du mit KeY quasi "nur" beweisen, dass u. bestimmten Annahmen von geltenden Invarianten (Assumed Invariants) vor Methodenaufruf sie auch nach Methodenaufruf (Ensured Invariants) gelten. Aber das ist bei 3.1 noch gar nicht gefordert.

Re: Lab4 Invarianten

Verfasst: 20. Feb 2013 18:06
von khaled
Das heißt das wir bei Task 3.1 einfach nur Invarianten eingeben müssen ohne dass wir die verifizieren?

Re: Lab4 Invarianten

Verfasst: 20. Feb 2013 18:14
von mmi1991
Zitat aus der Aufgabenstellung
Task 3
1. Read the class and field comments of class Highscore and class Record carefully and formalise them as JML invariants.
An der Stelle steht noch nichts von beweisen…

Wenn du die Aufgabenstellung weiterliest, merkst du auch, warum - das ist nämlich teilweise nicht ganz so einfach. Dazu musst du bei 3.2.5 nämlich nochmals die Einstellungen in KeY ändern, damit die Loop Invariante als solche erkannt wird. (btw ein Kommentar an den Veranstalter: Ich verstehe nicht ganz, warum man diese Einstellung in Task 1 (Preliminary) schon gemacht haben soll - schließlich sollte es ja eigentlich nicht schaden.)

Sprich beweisen kommt später in 3.2.

Re: Lab4 Invarianten

Verfasst: 20. Feb 2013 18:39
von khaled
Ok vielen dank :)