JML in KeY

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

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

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?

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

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.