PreservesInv: Assumed vs. Ensured Invariants

bluescreen
Neuling
Neuling
Beiträge: 3
Registriert: 29. Apr 2011 23:12

PreservesInv: Assumed vs. Ensured Invariants

Beitrag von 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?

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

Re: PreservesInv: Assumed vs. Ensured Invariants

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

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

Re: PreservesInv: Assumed vs. Ensured Invariants

Beitrag von 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
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 128
Registriert: 14. Apr 2011 22:52

Re: PreservesInv: Assumed vs. Ensured Invariants

Beitrag von 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
Mausschubser
Mausschubser
Beiträge: 64
Registriert: 13. Apr 2011 18:35

Re: PreservesInv: Assumed vs. Ensured Invariants

Beitrag von 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.

Antworten

Zurück zu „Archiv“