Hoare-Kalkül - böses Exemplar!

[carb]

Schaut euch mal das Hoare-Beispiel vom 29. Mai 2001 an. Beispiele dieser Art kommen öfter vor! Welchen Ansatz soll man denn da verwenden?? Irgendwie passt nämlich gar nix (durch dieses zweite "begin") ...

Hiiilfe!

mfg,
carb.

[Petzi]

hab mich auch schon gefragt, wie man das angeht
aber da gibt`s noch so ein grausiges Beispiel, wo "begin begin" vorkommt

muss mir diese Sachen noch gut anschauen

[sCHmIkOla]

irgendwie komm ich mit anschauen auch nicht auf einen grünen zweig

[Lukas]

sollte denke ich so funktionieren:

..... (der rest sollte dann eh klar sein)
(H4)___________________________________________
(P und x = x-y) (begin while x=0 do x<- 1; y <- y+x; end) R
(T1)_____________________________________________
P {begin x <- x - y; begin while x=0 do x <- 1; y <- y+x; end end}R

also man nimmt einfach an dass die schleife das &beta; bei regel T1 ist und löst sie erst beim zweiten schritt auf.

btw: nachdem ich euch da geholfen hab könntets ihr mir vielleicht bei dem problem mit AL (http://rs6k.feig.at/informatik-forum/showthread.php?s=&threadid=3422) helfen. gibts doch nicht dass das niemand weiss.... also falls jemand weiss wie das geht postets bitte eine antwort in den thread.

[carb]

T1 darf hier leider nicht angewendet werden: "v darf weder in P noch in t vorkommen."
v entspricht bei uns x,
t entspricht x - y

:(

[Lukas]

[edit] hab da vorher zwei regeln verwechselt... carb hat anscheinend doch recht, meine lösung dürft nicht stimmen.

[Petzi]

weiß niemand wie man sowas auflöst??

hab zwar schon herumprobiert, aber auf ein gutes Ergebnis bin ich leider noch nicht gekommen

ich hoff halt nur, dass er sowas morgen nicht gibt...

[carb]

stimmt, is ungut...
Die einzige Möglichkeit, die theoretisch besteht, ist (H2) anzuwenden. Wie kommt man dabei jedoch auf das Q??? Die drei Techniken, die im Scriptum angeführt sind, können gemäß der beschriebenen Voraussetzungen leider nicht angewandt werden. Sie würden ja auch nur zu den Formen (T1) bis (T3) führen.

Also wer hat eine Lösung?

[outsida]

also mit H2 würd das so ausschaun(etwas übersichtlicher vielleicht , sorry *g*)....

--------------------- (I^B)› I[-1/x]
----------------------------------------
----------(Q › I) ----- (I^B) {x <- 1} I ----- ((I^NOT B) › R[-y+x/y]
--------------------------------------------------------------
P › Q[-x-y/x] ------- Q{while x=0 do x <- 1;} R[-y+x/y]
------------------- -------------------------------------------------------
P{ x <- x - y} Q -------- Q{begin while x=0 do x <- 1; y <- y+x; end }R
-----------------------------------------------------------------------------------
P {begin x <- x - y; begin while x=0 do x <- 1; y <- y+x; end end}R



dann kann ich mir doch eigentlich aus P › Q[-x-y/x] ein Q ausrechnen, oder? (wie bei INV) .Laut Skriptum wird Q ja gewählt dh. es muß nur ein gültiger Wert sein, soweit ich das verstehe...
:confused:

[GetStoopid]

also soweit ich das verstanden hab muß in ner while mal grundsätzlich die formel in 3 teile zerlegt werden...
(siehe juniprf. und übungsbsp)
und das erste begin is glaub ich relativ egal, weils ja nur ne zuweisung auslöst, die man dann sowieso zur startbedingung hinzunimmt...

müßt irgendwie so aussehen

(P "und" x=x-y) impl. I__I{begin.... end}__I "und" B impl. Q


hoffe ich hab vielleicht bissl helfen können... (sofern ich net um 1:40 sowieso dämlich war und die frage komplett missverstanden hab *g* dann bitte ich um verzeihung) ;)

[carb]

WOW!!
Geschafft, es funzt tatsächlich mit (H2):

(H2) x<y^y=z {x<-x-y} Q ("a") ____ Q {begin ..... end} y=z+1 ("b")
---------------------------------------------------------------------------------------------------
(x<y^y=z) {begin x<-x-y; begin while x=0 do x<1; y<-y+x end end} y=z+1

Wenn man das wie gewohnt fortsetzt, nämlich bei "a" (H1), und bei "b" (T2), (H4) und (H1) anwendet, und als Invariante wie in der Angabe angegeben x<y ^ y=z verwendet, erhält man drei Formeln:

1.
x=0^y=z impl. x<2^y=z[x->1] ... stimmt offensichtlich

2.
x<2 ^ y=z ^ x!=0 impl. y=z+1[y->y+x]
linke Seite ergibt x=1, somit stimmt auch diese Aussage

3.
Q impl. x<2 ^ y=z

4.
x<y ^ y=z impl. Q[x->x-y]

nun wählt man Q = x<2 ^ y=z, somit stimmt 3. offensichtlich
durch einsetzen in 4. erhält man die Aussage:
x<y ^ y=z impl. x-y<2 ^ y=z
Entsprechend der Definition der Subtraktion über dem Datentyp N ergibt x-y bei x<y gleich 0
somit ist auch die letzte Formel eine Tautologie

BAMM, schwere Geburt..
is das alles irgendwie rübergekommen?

carb.

[carb]

Jetzt ist doch tatsächlich genau dieses Beispiel gekommen!! Oag! Ich hoff, die Lösung ist noch zu euch durchgedrungen. Mich hat der Beitrag von Outsida auf jeden Fall heute aussegrissn, weil ich mich dadurch noch mal mit dem Beispiel auseinandergesetzt habe, und es somit heute lösen konnte. *schwafel schwafel*

carb.

[-z0nk-]

verdammt ... total falsch ;-)

prüfung war überhaupt gemein ... hab nicht geglaubt, dass sequentialkalkül kommt :(

mfg, -z0nk-

[Petzi]

ich glaub mit dem Sequentialkalkül hat niemand gerechnet
hab mir schon gedacht, dass er DPLL geben wird

naja das Hoare Kalkül war zwar ein bissl fies, aber ich find, die Prüfung war im Großen und Ganzen zu schaffen

zum Glück hat er nicht so ein Beispiel geben, wo man ein Programm um eine for-Schleife oder so erweitern muss