PreservesInv: Assumed vs. Ensured Invariants

[bluescreen]

Hallo,

wenn man in Lab4, Task 2.6 eine Methode mit PreservesInv verifizieren will, erscheint ein Fenster mit zwei Tabs: Assumed Invariants und Ensured Invariants. Welche Invarianten müssen in welchem Fenster selektiert werden? D.h. wo muss die Invariante markiert sein, deren Einhaltung überprüft werden soll, und was wird im anderen Fenster ausgewählt?

[mmi1991]

Assume = etw. annehmen
Also diese Invarianten werden als gültig vor dem Methodenaufruf angenommen.

Ensure = etw. zusichern
Für diese Invarianten wird bewiesen, dass sie nach dem Methodenaufruf gültig sind, unter Zuhilfenahme von den assumed Invariants.

Alle Angaben ohne Gewähr

[Nathan Wasser]

Genau.

Ensured invariants sind die, deren Gültigkeit man nach Ausführung der Methode beweisen muss.

Assumed invariants sind die, von denen man vor Ausführung der Methode ausgehen will. Man kann hier prinzipiell alle selektiert lassen. Oft benötigt man aber hier nicht alle. Es kommt ganz darauf an was in der Methode passiert und welche Invariante man beweisen will.

Ein paar Beispiele:

Invariante #1: a >= 0
Invariante #2: b >= 0

Methode m: a = 5
Methode n: a++
Methode o: a = b
Methode p: a = a*b
Methode q: Ändert gar nicht den Wert von a

Um Invariante #1 zu Beweisen benötigen wir für:

Methode m: Gar keine Invarianten, da 5 offensichtlich >= 0 ist.
Methode n: Invariante #1, da a+1 >= 0 nur mit Hilfe der Aussage a >= 0 zu zeigen ist. (Mit Arithmetik Overflow ist das ganze gar nicht zu zeigen.)
Methode o: Invariante #2, denn b >= 0 ist genau Invariante #2. Insbesondere ist es hier egal was a vorher war, also wird Invariante #1 nicht benötigt.
Methode p: Beide Invarianten. (Mit Arithmetik Overflow ist das ganze gar nicht zu zeigen.)
Methode q: Invariante #1. Man denkt vielleicht zuerst, dass man keine Invariante benötigt, da sich der Wert nicht ändert, aber die Invariante muss genau aus diesem Grund ja vorher gegolten haben um danach immer noch zu gelten.

Man kann sich so leicht den Beweis aufs Nötigste reduzieren.

[hstr]

Wir haben hier ein Problem mit der Aufgabe 2.5 bzw. 2.6, und zwar haben wir die Methoden won() und isPossible() entsprechend dem Vertrag implementiert.
Jetzt haben wir versucht alle Invarianten seperat zu beweisen, hierzu haben wir alle Invarianten unter Assumed Invariants markiert und die Ensured Invariants einzeln selektiert.
Bei allen 3 Methoden, won(), isPossible() und move() ist es uns nicht möglich die Invariante

Code: Alles auswählen

/*@ 
public invariant 
(\exists int colNr; colNr >= 0; 
(\forall int row; row >= 0 && row < maze.length;
maze[row].length == colNr));
@*/    

zu beweisen. Alle anderen Invarianten, bis auf eine bei move() lassen sich aber beweisen.
Das kann aber eigentlich nicht sein, da keine der 3 Methoden die Dimension des Maze verändert.

Habt ihr das Problem auch?

[tacu]

Das kann aber eigentlich nicht sein, da keine der 3 Methoden die Dimension des Maze verändert.

Habt ihr das Problem auch?

sieht bei uns genauso aus, haben auch keine ahnung wie das entsteht.