JML in KeY

hstr
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 128
Registriert: 14. Apr 2011 22:52

JML in KeY

Beitrag von hstr »

Hallo,
wir stellen uns gerade die Frage, wie man mit KeY z.B. die Invariante 4 "each cell inside the maze is either free, a wall or an exit." überprüfen soll.
Die JML Formel ist dabei nicht das Problem, aber woher soll KeY wissen, dass der Eingabebereich nur von 0-2 geht.
Der Wertebereich des Integer Arrays maze ist ja der gesamte Integer Bereich. Man könnte genau so auf Werte zwischen 3-5 überprüfen.
Den Eingabebereich bereits in der Vorbedingung einzuschränken ist ja irgendwie sinnlos.
Key müsste also feststellen, mit welchen Werten maze instanziiert wird.

Benutzeravatar
JannikV
Nerd
Nerd
Beiträge: 609
Registriert: 24. Apr 2011 12:42

Re: JML in KeY

Beitrag von JannikV »

Das habe ich mir auch schon gedacht. Ich denke die Invarianten werden nicht direkt bewiesen, wie auch. Vielleicht höchstens auf Konsistenz geprüft, also ob das überhaupt möglich ist was man da will. Aber bevor der Konstruktor durchgelaufen ist, kann man das in der Tat nicht sagen.
Denkbar wäre natürlich dass man den Konstruktor so implementiert, dass er nur Arrays annimmt die die Eigenschaft erfüllen. Das macht der bereits implementierte Konstruktor aber nicht. Trotzdem verifiziert KEY alles schön. Also scheint das ganze anders zu funktionieren als wir es uns vorstellen.
Mal hoffen dass sich der Veranstalter mal meldet oder wir in der nächsten Vorlesung was dazu gesagt bekommen. Invarianten kamen bisher ja generell noch nicht dran..

VG

null
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 168
Registriert: 21. Apr 2012 14:58

Re: JML in KeY

Beitrag von null »

Wurde nicht in der Vorlesung gesagt, dass man für FO- Ausdrücke eine Bedinung angeben kann. Also etwa so:

/*@invariant \forall int x; x < maze.length; blabla @*/

Der mittlere Teil kann x einschränken. Oder?

Benutzeravatar
JannikV
Nerd
Nerd
Beiträge: 609
Registriert: 24. Apr 2011 12:42

Re: JML in KeY

Beitrag von JannikV »

Das ist jetzt aber ne neue Frage und hat nichts mit dem zu tun was hstr gefragt hat oder?

Die Antwort ist ja, aber um die Qantorenausdrücke müssen Klammern gesetzt werden. Also etwa so

Code: Alles auswählen

//@ public invariant (\forall int i; i < bound; someStatement);
VG

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

Re: JML in KeY

Beitrag von Nathan Wasser »

Also, erstens sollt ihr gar nichts mit KeY überprüfen, ihr sollt lediglich JML Spezifikationen schreiben.

Zweitens gibt es am 15. Januar noch eine JML Vorlesung.

Antworten

Zurück zu „Archiv“