Lab4 Invarianten

[khaled]

Hallo,
Kann mir jemanden sagen wie ich die Invarianten ( in Task3.1 ) in KeY verifizieren kann.

Khalid

[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.

[khaled]

Das heißt das wir bei Task 3.1 einfach nur Invarianten eingeben müssen ohne dass wir die verifizieren?

[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.

[khaled]

Ok vielen dank