wp-kalkül

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.

wp-kalkül
hi leute…

bin am rätseln aber bekomms net hin:

wp(if (a>b) c:= d; else e:= f; , c=7 & e=f & a=4 & b=6) =

kann mir das vll kurz jemand hinschreiben wie ich des durchrechne?s


hi, also ich blick die sache auch nicht so wirklich, aber meine lösung würde so aussehen:
… =
(hier die if-then-else-Regel anwenden → skript)
= [(a>b) & wp(c:=d, c=7&e=f&a=4&b=6)] OR [(a<=b) & wp(e:=f, c=7&e=f&a=4&b=6)] =
(nun noch die wps auflösen)
= [(a>b) & (d=7 & e=f & a=4 & b=6)] OR [(a<=b) & (c=7 & a=4 & b=6)]

und weiter komm ich auch nicht… ich hab also nur die if-regel angewandt und beim wp eingesetzt: zB. wp(c:=d, c=7) = (d=7)

Wäre auch froh über weitere erläuterungen =)


Bis dahin hab ichs auch so wie du, sac. Dann kann man glaub ich noch wie folgt weitervereinfachen:

… = false OR (c=7 AND a=4 AND b=6)

denn a>b AND (a=4 AND b=6) ergibt false. Wie man aber dann weitermacht, weiss ich auch nicht.

EDIT: Wahrscheinlich ist das dann einfach c=7 AND a=4 AND b=6


Meine Theorie:

Schritt 1: if-Regel
Schritt 2: Zuweisungsregel

Kann man gleich recht nett zusammen machen:

[a>b & d=7 & e=f & a=4 & b=6] |
[!(a>b) & c=7 & f=f & a=4 & b=6]

Da [m](a=4 & b=6) → !(a>b)[/m] ist Zeile 1 falsch und fällt aus der Disjuktion weg. In Zeile 2 gilt natürlich das gleiche, deshalb ist [m]!(a>b) = true[/m], ebenso wie [m]f=f[/m], und da das Ganze eine große Konjuktion ist, fallen die beiden raus.

Bleibt also:
[m]wp(…) <=> c=7 & a=4 & b=6[/m]


stimmt ja! hab das völlig übersehen… viel weiter geht das dann glaube ich nicht mehr.


es ist doch so, dass die erste Zeile “false” ist. die zweite Zeile müsste doch dann bei !a>b true sein, wie schon oben erwähnt. da zwischen diesen beiden Zeilen jetzt der operator “oder” steht entsteht doch eigentlich “false oder true” und das müsste doch dann “true” sein oder lieg ich da jetz völlig aufm falschen dampfer?

oh sorry, hab grad gesehn, ihr habts richtig!


[m]!(a>b)[/m] ist tatsächlich true. Allerdings macht das z.B. [m]!(a>b) & false[/m] noch nicht wahr.
[m]!(a>b)=true[/m] kann man also weglassen, aber nicht gleich auch die restlichen Dinger, die noch zu der “Verundung” gehören ([m]A & true <-> A[/m])


hmm, kein plan, ich hatte da ne ganz andere idee ^^

wp(if (a>b) c:= d; else e:= f; , c=7 & e=f & a=4 & b=6) =
c=7 & a<=b & a=4 & b=6

da die nachbedingung e=f gilt, kann ich davon ausgehen, dass die if bedingung in den else fall gegangen ist, und deswegen a<=b war.
[edited]

… aber das ist meine einschätzung ^^ hab mich dem wp-Kalkül auch nicht so intensiv beschäftigt.


In einem Kalkül kommt’s einfach nur darauf an, stur ein paar Regeln zu befolgen. Nachdenken ist ganz falsch… :smiley:


naja, aber immerhin gibt mir die Lösung recht :slight_smile: … in der es auch heisst:


Naja, das [m]a<=b[/m] könnte man noch weglassen…

Ich würd mir an deiner Stelle einfach noch einmal die paar Regeln (–> Sequenzregel, Zuweisungsregel, if-Regel) anschauen, und dann macht sich so eine Aufgabe eh schon fast von alleine… :slight_smile:


jo, immoartl, das a <= b kann man weg lassen, da man ja a = 4 und b = 6 voraussetzt, und das somit erfüllt is. Ham das vorgestern mal mit Frozy bissl durchgemacht.


eigentlich muesste dann auch das a=4 und b= 6 wegfallen und nur noch c=7 uebrig bleiben…der rest der aussage is naemlich = true…


nein, weil du, wenn du a = 4 und b = 6 wegfallen lässt, ja praktisch sagst, dass du für a nen beliebigen wert und für b nen beliebigen wert einsetzen kannst, was aber dann nich mehr stimmt…


aber mal so ne grundsätzliche frage: was bringt mir das wp kalkül wann? also was kann ich damit bezwecken? Irgendwie is mir die essenz noch nich so ganz klar geworden…
(also schon dass ich die schwächste Vorbedingung krieg, wenn ich in die Ausdrücke meine nachbedingung einsetz, aber ansonsten?)


Du kannst damit beweisen, dass dein Algorithmus das richtige tut…


Wenn du beweisen kannst, dass unter der Vorbedingung P dein Algorithmus nach seinem Durchlaufen die gewünschte Nachbedingung Q erfüllt und er zusätzlich (immer) terminiert hast du die totale Korrektheit deines Algorithmus bewiesen.
Falls du die Terminierung nicht beweist (was manchmal sehr schwierig / unmöglich ist), hast du die partielle Korrektheit deines Algorithmus bewiesen.
:finger: