Lab4 Invarianten

khaled
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 102
Registriert: 28. Mai 2012 01:16

Lab4 Invarianten

Beitrag von khaled »

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

Khalid

Benutzeravatar
mmi1991
Computerversteher
Computerversteher
Beiträge: 349
Registriert: 20. Okt 2011 18:46
Wohnort: Hattersheim

Re: Lab4 Invarianten

Beitrag 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.
Ophasentutor SoSe 2014, WiSe 2015/16
Alle Angaben wie immer ohne Gewähr

khaled
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 102
Registriert: 28. Mai 2012 01:16

Re: Lab4 Invarianten

Beitrag von khaled »

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

Benutzeravatar
mmi1991
Computerversteher
Computerversteher
Beiträge: 349
Registriert: 20. Okt 2011 18:46
Wohnort: Hattersheim

Re: Lab4 Invarianten

Beitrag 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.
Ophasentutor SoSe 2014, WiSe 2015/16
Alle Angaben wie immer ohne Gewähr

khaled
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 102
Registriert: 28. Mai 2012 01:16

Re: Lab4 Invarianten

Beitrag von khaled »

Ok vielen dank :)

Antworten

Zurück zu „Archiv“