wp-Kalkül allgemein

[system]

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

[lemur]

wp-Kalkül allgemein
Hi,

in den ganzen Musterlösungen zu den Klausuren wird der Beweis, dass die Schleifeninvariante gilt, immer so
bewiesen:
{I ∧ b} => wp(A,I)
und dann
¬{I ∧ b} ∨ wp(A,I)
Wenn ich’s richtig verstehe, ist das ja einfach nur Boolesche Logik, oder?
Ich frage mich aber, ob man das so machen muss, oder ob man nicht auch wie in den Vorlesungsfolien
erst wp(A,I) und dann I ∧ b so weit es geht auflöst und dann evtl mit ein, zwei Sätzen argumentieren kann,
dass I ∧ b stärker als wp(A,I) ist und somit die Schleifeninvariante gilt.

[JohnDoe]

---

@lemur

in den ganzen Musterlösungen zu den Klausuren wird der Beweis, dass die Schleifeninvariante gilt, immer so
bewiesen:
{I ∧ b} => wp(A,I)
und dann
¬{I ∧ b} ∨ wp(A,I)
Wenn ich’s richtig verstehe, ist das ja einfach nur Boolesche Logik, oder?
Ich frage mich aber, ob man das so machen muss,

nein, muss man nicht

@lemur

oder ob man nicht auch wie in den Vorlesungsfolien erst wp(A,I) und dann I ∧ b so weit es geht auflöst und dann

ja, darf man auch

@lemur

evtl mit ein, zwei Sätzen argumentieren kann,

NEIN, DARF MAN NICHT
(edit: sorry, wollte euch nicht anschreien - aber bei jeder Korrektur ist es dann doch wieder zum Schreien…)

@lemur

dass I ∧ b stärker als wp(A,I) ist und somit die Schleifeninvariante gilt.

ja, kann man auch - solange es formal mittels wp-Kalkül ist…

[JohnDoe]

---

[lemur]

---

Das heißt, angenommen, ich bekomme bei wp(A,I) raus: x > 0 und bei {I ∧ b}: x >= -1.
Dann ist ja {I ∧ b} stärker als wp. In den Vorlesungsfolien sind da dann Pfeile auf die einzelnen
Ausdrücke und es steht noch daneben “Vorbedingung kann verschärft werden”. Wie sollte man
das dann formal mittels wp-Kalkül hinschreiben?
Danke übrigens für die schnelle Antwort

[ferdi0807]

---

Ich bin mir nicht sicher, ob es dir hilft, aber auf den Folien 9-83 bis 9-85 habe ich es mir ein wenig zusammengereimt.

[JohnDoe]

---

@lemur

Das heißt, angenommen, ich bekomme bei wp(A,I) raus: x > 0 und bei {I ∧ b}: x >= -1.
Dann ist ja {I ∧ b} stärker als wp.

ähm, nö… andersrum!
Eselsbrücke (Annahme: x sei ganzzahlig!): wp(A,I): x>0 ist soooo stark, das schließt sogar x = -1 und x = 0 aus, während {I ∧ b}: x >= -1 diesbezüglich „schwächelt“…
Edit/PS: das ist ein Zeichen, dass man sich verrechnet oder die falsche I gewählt hat :(…

@lemur

In den Vorlesungsfolien sind da dann Pfeile auf die einzelnen
Ausdrücke und es steht noch daneben „Vorbedingung kann verschärft werden“. Wie sollte man
das dann formal mittels wp-Kalkül hinschreiben?
Danke übrigens für die schnelle Antwort

Sauber wäre es, die beiden Ausdrücke formal und schrittweise so umzuformen, dass man die einzelnen Teilausdrücke jeweils beim anderen wiedererkennt und dann die richtige Implikation oder gar Äquivalenz dazwischen zu setzen.
Auf F. 9-115 hätte es genügt, statt der vielen kleinen Pfeile einfach ein „<=“ [Implikation in die Richtung: {I ∧ b} => wp(A,I)] zu setzen, was aber didaktisch (aka zur Nachbereitung ;)) weniger nachvollziehbar gewesen wäre…

[lemur]

---

Ok,
ich glaube, ich habe dann alles so weit verstanden, dass die Implikation andersrum hätte sein müssen, verstehe ich
auch.
Dankeschön