3.3 Loop Invariant

FGB
Mausschubser
Mausschubser
Beiträge: 45
Registriert: 21. Jan 2006 14:41
Wohnort: Darmstadt
Kontaktdaten:

3.3 Loop Invariant

Beitrag von FGB » 13. Feb 2014 15:18

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

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

Re: 3.3 Loop Invariant

Beitrag von Nathan Wasser » 13. Feb 2014 15:57

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.

FGB
Mausschubser
Mausschubser
Beiträge: 45
Registriert: 21. Jan 2006 14:41
Wohnort: Darmstadt
Kontaktdaten:

Re: 3.3 Loop Invariant

Beitrag von FGB » 13. Feb 2014 16:04

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

FGB
Mausschubser
Mausschubser
Beiträge: 45
Registriert: 21. Jan 2006 14:41
Wohnort: Darmstadt
Kontaktdaten:

Re: 3.3 Loop Invariant

Beitrag von FGB » 14. Feb 2014 15:11

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

rindphi
Mausschubser
Mausschubser
Beiträge: 55
Registriert: 3. Sep 2009 20:52
Kontaktdaten:

Re: 3.3 Loop Invariant

Beitrag von rindphi » 14. Feb 2014 16:21

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!

FGB
Mausschubser
Mausschubser
Beiträge: 45
Registriert: 21. Jan 2006 14:41
Wohnort: Darmstadt
Kontaktdaten:

Re: 3.3 Loop Invariant

Beitrag von FGB » 17. Feb 2014 23:29

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?

rindphi
Mausschubser
Mausschubser
Beiträge: 55
Registriert: 3. Sep 2009 20:52
Kontaktdaten:

Re: 3.3 Loop Invariant

Beitrag von rindphi » 18. Feb 2014 18:11

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.

Antworten

Zurück zu „Archiv“