Hallo,
Kann mir jemanden sagen wie ich die Invarianten ( in Task3.1 ) in KeY verifizieren kann.
Khalid
Lab4 Invarianten
Re: Lab4 Invarianten
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.
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.
Ophasentutor SoSe 2014, WiSe 2015/16
Alle Angaben wie immer ohne Gewähr
Alle Angaben wie immer ohne Gewähr
Re: Lab4 Invarianten
Das heißt das wir bei Task 3.1 einfach nur Invarianten eingeben müssen ohne dass wir die verifizieren?
Re: Lab4 Invarianten
Zitat aus der Aufgabenstellung
Task 3
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.
Task 3
An der Stelle steht noch nichts von beweisen…1. Read the class and field comments of class Highscore and class Record carefully and formalise them as JML invariants.
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.
Ophasentutor SoSe 2014, WiSe 2015/16
Alle Angaben wie immer ohne Gewähr
Alle Angaben wie immer ohne Gewähr
Re: Lab4 Invarianten
Ok vielen dank 
