Seite 1 von 1

3.3 Loop Invariant

Verfasst: 13. Feb 2014 15:18
von FGB
Moin zusammen,

ich stehe ein wenig auf dem Schlauch bzgl. des Problems 3.3a.

Ich habe es geschafft, drawMultiple() zu beweisen, ohne eine Invarante anzugeben. Denke aber das ist nicht Sinn und Zweck der Aufgabe ("Prove that the method drawMultiple() preserves the invariants")

Ich schaffe es soweit, dass ich für die while-Schleife der drawVertical eine "Loop Invariante" angeben muss. Hier hört mein "Verständnis" leider auf.
Wahrscheinlich habe ich die Invarianten allgemein nicht ganz verstanden. Ich war zwar in der Vorlesung, erinnere mich auch, dass der Dozent recht schnell immer eine Invariante angegeben bzw. editiert hat. Aber was genau er dort gemacht hat ...

Hat mir jemand einen Tipp?

Danke und Grüße
Felix

Re: 3.3 Loop Invariant

Verfasst: 13. Feb 2014 15:57
von Nathan Wasser
Es gibt einen großen Unterschied zwischen Klassen-/Instanz-Invarianten und Schleifeninvarianten.

In 3.3a soll man etwas beweisen, dazu ist es nicht erforderlich eine Invariante anzugeben, denn diese gibt es bereits. Ausserdem sollte man sich bei dieser Aufgabe auch nicht auf Schleifeninvarianten stützen, denn wie in (b) geschrieben ist die angegebene Schleifeninvarianten eh nicht vollständig korrekt.

In 3.3b soll wieder etwas bewiesen werden. Hierzu wird es nötig sein die Schleifeninvariante zu nutzen. Diese ist - wie jetzt schon zum dritten mal erwähnt - nicht ganz richtig. Demnach muss man sie abändern.

Also: Es sind in der Aufgabe keinerlei Invarianten anzugeben. Verstehen, benutzen, modifizieren, beweisen: ja. Angeben: nein.

Hoffe das hilft.

Re: 3.3 Loop Invariant

Verfasst: 13. Feb 2014 16:04
von FGB
Danke Nathan,

3.3a konnte ich ja in KeY beweisen. Sprich damit bin ich fertig.
3.3b setze ich mich gleich mal ran.

Danke und GRüeß
Felix

Re: 3.3 Loop Invariant

Verfasst: 14. Feb 2014 15:11
von FGB
Hi zusammen,

habe irgendwie Probleme mit der Aufgabenstellung, wo mir der Tutor leider auch nicht weiterhelfen kann:

"[...] Hint: The goal "Initially Valid" can be closed using "apply rules automatically here". [...]"

Nach dem Ausführen von "apply rules automatically here" bei "Invariant Initally Valid" habe ich leider mehr offene Ziele ...

Stimmt die Aufgabenstellung nicht, oder mache ich was falsch?

Danke und Grüße
Felix

Re: 3.3 Loop Invariant

Verfasst: 14. Feb 2014 16:21
von rindphi
FGB hat geschrieben:habe irgendwie Probleme mit der Aufgabenstellung, wo mir der Tutor leider auch nicht weiterhelfen kann:

"[...] Hint: The goal "Initially Valid" can be closed using "apply rules automatically here". [...]"

Nach dem Ausführen von "apply rules automatically here" bei "Invariant Initally Valid" habe ich leider mehr offene Ziele ...

Stimmt die Aufgabenstellung nicht, oder mache ich was falsch?
Ich glaube, ich bin der entsprechende Tutor ;)
Gerade habe ich es noch einmal getestet, und es geht. Wende "apply rules automatically here" auf das gesamte Goal bei "Invariant Initally Valid" an, direkt nach dem du "Loop Invariant -> Apply rule" ausgewählt hast. Dann sollte es gehen.

Es war gerade leider echt wenig Zeit in der Übung, sonst hätte ich dir den Hinweis wohl auch gleich geben können. Das Lernziel besteht hier auf jeden Fall in der Korrektur der Invariante, die für den Preserves und Use Case-Fall fehlschlägt.

Viel Erfolg noch!

Re: 3.3 Loop Invariant

Verfasst: 17. Feb 2014 23:29
von FGB
Hi,

danke für den Tipp :) So hat er die "initally Valid"-Goals geschlossen.

Nur leider ist danach schluss. Ich finde wohl nicht den Fehler ... Obwohl ich dachte ihn gefunden zu haben.
Nach meinem VErständnis habe ich einen Fehler beim Assignable gefunden, und einen in der Invarianten-Definition (\for ...)

Es gibt ja den Hinweis, dass man nach dem CUT abschneiden soll. PRoblem ist nur, dass mein CUT vollständig geschlossen wird. Habe nur noch 2 offene Ziele bei "Body PReserves Invariant" und "Use Case".

Wenn man den FEhler gefunden und korrigiert hat, müsste dann KeY problemlos (bis auf 1 x Invariante anwenden und "apply rules auto...") durchlaufen?

Re: 3.3 Loop Invariant

Verfasst: 18. Feb 2014 18:11
von rindphi
FGB hat geschrieben:Hi, danke für den Tipp :) So hat er die "initally Valid"-Goals geschlossen.
Schön! :)
FGB hat geschrieben:Wenn man den FEhler gefunden und korrigiert hat, müsste dann KeY problemlos (bis auf 1 x Invariante anwenden und "apply rules auto...") durchlaufen?
Ja, er sollte dann ansonsten automatisch durchlaufen. Denke daran, dass du evtl. bei zu kleiner Suchtiefe mehrere Male auf "Play" drücken musst. Die Invariante muss dann natürlich korrekt sein... Und es existiert garantiert ein Fehler in der eigentlichen Invariante, d.h. Korrektur eines eventuellen Fehlers im assignable-Clause reicht nicht aus.