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?
PreservesInv: Assumed vs. Ensured Invariants
-
- Neuling
- Beiträge: 3
- Registriert: 29. Apr 2011 23:12
Re: PreservesInv: Assumed vs. Ensured Invariants
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
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

Ophasentutor SoSe 2014, WiSe 2015/16
Alle Angaben wie immer ohne Gewähr
Alle Angaben wie immer ohne Gewähr
-
- Kernelcompilierer
- Beiträge: 430
- Registriert: 16. Okt 2009 09:48
Re: PreservesInv: Assumed vs. Ensured Invariants
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.
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.
Re: PreservesInv: Assumed vs. Ensured Invariants
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
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?
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));
@*/
Das kann aber eigentlich nicht sein, da keine der 3 Methoden die Dimension des Maze verändert.
Habt ihr das Problem auch?
Re: PreservesInv: Assumed vs. Ensured Invariants
sieht bei uns genauso aus, haben auch keine ahnung wie das entsteht.Das kann aber eigentlich nicht sein, da keine der 3 Methoden die Dimension des Maze verändert.
Habt ihr das Problem auch?