Lab4 - Probleme mit HighscoreSorted Invariante und insertAt

L4_
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 104
Registriert: 24. Apr 2012 15:44

Lab4 - Probleme mit HighscoreSorted Invariante und insertAt

Beitrag von L4_ »

Hallo,

die Invariante quantifiziert über Elemente mit index 0 bis size-1 und beschreibt die Sortierung (jedoch ohne Ausschluss von "null"-Elementen).

Die Methode insertAt erlaubt es einen Record überall hinzuzufügen, auch wenn size != capacity.
Bsp:

Size := 2
Capacity := 5
in := { R2, R1, null, null, null }

Wenn ich nun insertAt(R3, 3, in) aufrufe, habe ich folgendes Ergebnis:

in := { R2, R1, null, R3, null } und Size = 3

Nun würde müsste in der Invariante sowas wie NullPointerException geben, da in[2] == null und mit diesem element auf ".score" zugegriffe wird.

Jedenfalls habe ich das Problem, dass mein EnsuresPost-Proof von insertAt nicht schließt, selbst wenn ich "loop_invariant true" setze.
Liegt hier nun ein Fehler in der Implementierung vor oder wo liegt das Problem?

VG

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

Re: Lab4 - Probleme mit HighscoreSorted Invariante und inser

Beitrag von mmi1991 »

Die Loop-Invariante spezifizierst du deshalb, damit KeY rausfinden kann, was bei jedem Schleifendurchlauf gleich bleibt.
Das sind also quasi zusätzliche Informationen, die du KeY vermittelst, um beim Beweis zu helfen.

Folglich ist es nicht verwunderlich, dass der Beweis nicht schließt, wenn du Loop-Invariant true benutzt.
Ophasentutor SoSe 2014, WiSe 2015/16
Alle Angaben wie immer ohne Gewähr

L4_
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 104
Registriert: 24. Apr 2012 15:44

Re: Lab4 - Probleme mit HighscoreSorted Invariante und inser

Beitrag von L4_ »

-
Zuletzt geändert von L4_ am 20. Feb 2013 17:14, insgesamt 1-mal geändert.

L4_
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 104
Registriert: 24. Apr 2012 15:44

Re: Lab4 - Probleme mit HighscoreSorted Invariante und inser

Beitrag von L4_ »

Du missverstehst mich.
Ich habe nicht geschrieben, dass ich die Aufgabe mit "loop_invariant true;" lösen will.
Ich habe auch nicht gefragt, weshalb ich die loop-variante spezifiziere.

Ich wollte damit lediglich sagen, dass der Beweis selbst damit nicht schließt (obwohl er das doch tun müsste, sofern die Loop_invariant nie false wird).
Meine richtige loop_invariante habe ich natürlich sinnvoll definiert.

Die Invariante die ich anspreche ist die ganz oben in der Klasse (nicht loop_invariante!).

yourmaninamsterdam
Nerd
Nerd
Beiträge: 681
Registriert: 26. Okt 2006 14:04
Kontaktdaten:

Re: Lab4 - Probleme mit HighscoreSorted Invariante und inser

Beitrag von yourmaninamsterdam »

Ich glaube, mmi1991 hat dich schon richtig verstanden. Um EnsuresPost für eine Methode zu beweisen brauchst du doch die Nachbedingung einer Schleife. Wenn du die Invariante da auf true setzt, mag das nie false sein, es generiert aber auch keine sinnvolle Nachbedingung, die für den Rest der Methode verwendet werden kann.

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

Re: Lab4 - Probleme mit HighscoreSorted Invariante und inser

Beitrag von Nathan Wasser »

L4_ hat geschrieben:Ich wollte damit lediglich sagen, dass der Beweis selbst damit nicht schließt (obwohl er das doch tun müsste, sofern die Loop_invariant nie false wird).
Das ist nicht korrekt. Wenn die Loop-Invariante true wäre, dann wüsste man am Ende der Schleife, dass true = true ist und sonst nichts. Dies ist nicht sonderlich hilfreich um etwas zu beweisen was keine Tautologie ist.

L4_
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 104
Registriert: 24. Apr 2012 15:44

Re: Lab4 - Probleme mit HighscoreSorted Invariante und inser

Beitrag von L4_ »

Nungut, dann scheint es wohl mit der Invariante in Codezeile 5-8 keine Probleme zu geben.

Ich habe mir "Ensures" von insertAt angeschaut und habe in der Loop-invariant gefordert, dass dies auch in jeder Iteration gelte (natürlich angepasst an die Laufvariable "start").
Dachte eigentlich, das wäre bereits alles, jedoch scheint dies wohl nicht der Fall zu sein.
Weiß auch nicht recht, was ich sonst übersehe... ggf. noch Ideen?

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

Re: Lab4 - Probleme mit HighscoreSorted Invariante und inser

Beitrag von Nathan Wasser »

L4_ hat geschrieben:die Invariante quantifiziert über Elemente mit index 0 bis size-1 und beschreibt die Sortierung (jedoch ohne Ausschluss von "null"-Elementen).

Wenn ich nun insertAt(R3, 3, in) aufrufe, habe ich folgendes Ergebnis:

in := { R2, R1, null, R3, null } und Size = 3

Nun würde müsste in der Invariante sowas wie NullPointerException geben, da in[2] == null und mit diesem element auf ".score" zugegriffe wird.
Was du hier richtig erkannt hast ist, dass die Methode insertAt diese Invariante nicht einhält. (Das ist eigentlich auch nicht ganz korrekt, aber es ist auf alle Fälle nicht zu beweisen, dass die Methode die Invariante einhält.)

Die Spezifikation der insertAt Methode hätte also durchaus besser gewählt werden können. Glücklicherweise hindert das aber nicht an der erfolgreichen Bearbeitung der Bonusaufgabe, da hier nur nach dem Beweis von ensuresPost gefragt wurde und nicht preservesInv. Man darf also davon ausgehen, dass die Invariante vor der Methode gilt und muss nur beweisen, dass die Postcondition nach der Methode stimmt, die Einhaltung der Invariante ist also für diesen Beweis egal.

Noch ein Punkt: Invarianten werfen keine NullpointerExceptions oder ähnliches. Es gibt einen Wert für null.score, man kann nur nichts darüber sagen. Ihr braucht euch damit nicht zu beschäftigen, aber ich muss es leider erwähnen. :)

Das Problem liegt sehr wahrscheinlich bei deiner Wahl der Loop Invariante. Das soll auch kein Vorwurf sein, es ist sehr schwierig auf Anhieb das richtige zu finden. Gehe bitte wie folgt vor:

1. Stelle sicher, dass deine Loop Invariante gelesen wird, also die // Kommentare innerhalb der JML Spezifikation weg sind.
2. Formuliere eine Loop Invariante, die tatsächlich die Postcondition zeigen kann. (KeY sollte also nach Benutzung der Loop Invariant zumindest mal den Use Case Fall beweisen können.)
3. Stelle sicher, dass die Invariante vor der Schleife gilt. (KeY muss den Invariant Initially Valid Fall beweisen können.)
4. Der schwierigste Teil: Der Body Preserves Invariant Fall sollte auch beweisbar sein.

Wenn eines oder mehrere der 3 Fälle nicht automatisch zu beweisen sind, war die Invariante höchstwahrscheinlich falsch. Nochmal überdenken was alles gelten muss, bzw was nicht unbedingt in allen Fällen erforderlich ist. Eine Invariante, die zumindest 2. & 3. erfüllt ist vermutlich schon mal auf dem richtigen Weg und muss nur noch verfeinert werden. Wenn eines dieser Fälle aber nicht zu beweisen sind, sollte nochmal gründlich überlegt werden wo das Problem liegt.

Ein letzter Tipp: "assignable in[at+1..in.length-1], start;" bedeutet, dass diese Variablen nach jedem Schleifendurchgang prinzipiell beliebige Werte haben können. Deine Invariante muss also stark genug sein, um diesen Chaos entgegen wirken zu können.

L4_
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 104
Registriert: 24. Apr 2012 15:44

Re: Lab4 - Probleme mit HighscoreSorted Invariante und inser

Beitrag von L4_ »

Dein letzter Hinweis ließ gab mir dann noch ein paar Ideen :) Jedoch kommen mir nun folgende Fragen auf:

Wenn ich in der Loop_invariante \old benutze z.B. in == \old(in), bedeutet das nun dass \old(in) vor der Iteration und in nach der Iteration ist?
Sprich, dass das aktuelle und alte Objekt immer von der Iteration abhängt?
Oder ist "old" vor Schleifenbeginn und "aktuell" nach Terminierung?

Ich versuche ja zu sagen, dass immer alle Elemente bis "at" unverändert bleiben, bis auf genau Element, welches in einer Iteration überschrieben wurde.
Initially Valid gilt mit meiner invariante auch, aber irgendwie scheint ihm das nicht zu langen.
Ich sehe irgendwie nicht den Fehler und es fällt mir leider auch schwer mit KeY nachzuvollziehen, woran es hängt... naja, mal gucken, ggf. gebe ich nur das ab, was ich soweit habe.

errt
Mausschubser
Mausschubser
Beiträge: 61
Registriert: 18. Okt 2012 19:12

Re: Lab4 - Probleme mit HighscoreSorted Invariante und inser

Beitrag von errt »

Nachdem wir unsere Invariante entsprechend formuliert haben und das funktionierte, würde ich behaupten, \old ist der Zustand vor dem ersten Schleifeneintritt, alles andere wird im jeweils aktuellen Kontext, also zu jeder Iteration ausgewertet.

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

Re: Lab4 - Probleme mit HighscoreSorted Invariante und inser

Beitrag von Nathan Wasser »

L4_ hat geschrieben:Wenn ich in der Loop_invariante \old benutze z.B. in == \old(in), bedeutet das nun dass \old(in) vor der Iteration und in nach der Iteration ist?
Sprich, dass das aktuelle und alte Objekt immer von der Iteration abhängt?
Oder ist "old" vor Schleifenbeginn und "aktuell" nach Terminierung?


Weder noch. \old(x) bedeutet der Wert von x vor Methodenaufruf, x bedeutet der Wert von x jetzt. Das heißt in Initially Valid ist x der Wert vor der Schleife, in Use Case ist x der Wert nach der Schleife und in Body Preserves Invariant ist x der Wert vor (wenns vor dem Code steht), bzw nach (wenns nach dem Code steht) irgendeiner Iteration.

Da die Methode vor der Schleife keine Änderungen an in vornimmt, ist in diesem Spezialfall \old(in) natürlich schon auch der Wert vor der Schleife, aber das ist nicht die Definition.

L4_
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 104
Registriert: 24. Apr 2012 15:44

Re: Lab4 - Probleme mit HighscoreSorted Invariante und inser

Beitrag von L4_ »

Oh man - ich habs wohl in der zwischenzeit iwann richtig gehabt, nur dann nicht gemerkt, dass an meinem PC Anzahl Knoten auf 1000 eingestellt war und nicht auf 10000 oder mehr. Daher dachte ich, dass der Beweis nie geklappt hat.
Auf meinem Notebook gings nämlich heut wie ich zufällig entdeckte.

Zu blöd, wenn die Ursache ganz wo anders liegt als beim eigentlichen Problem x)

Danke dennoch soweit!

Antworten

Zurück zu „Archiv“