10.5

[Erendis]

also irgendwie komm ich hier nicht weiter, ich kann nur 2 Hoare Gesetze anwenden, nämlich H4 und H3.
könnte mir da jemand weiterhelfen?? :engel:

[kambo]

ich kann zumindest versuchen....

H4, H3 , H1 =>

(1) P impliziert I ( wo I= (P oder Q) )
(2) ((I and B) and eq?(x, y)) impliziert I [build(x,y) | x ])
(3) ((I and B) and NOTeq?(x,y) impliziert I [build(x, x) | x])
(4) (I and NOT B) impliziert Q)

[ein_stein2000]

ich kann zumindest versuchen....

H4, H3 , H1 =>

(1) P impliziert I ( wo I= (P oder Q) )
(2) ((I and B) and eq?(x, y)) impliziert I [build(x,y) | x ])
(3) ((I and B) and NOTeq?(x,y) impliziert I [build(x, x) | x])
(4) (I and NOT B) impliziert Q)<blödsinn, stimmt net> i glaub du hast an fehler bei (2) und (3) gemacht! da gehört jeweils (I and notB) and .... </blödsinn> => stimmt alles, siehe meinen post #6 (http://hades.gothic.at/iforum/showpost.php?p=136347&postcount=6)

aber näheres siehe bitte meine pdf ... ich weiß leider net wie ich 2 und 3 ausrechnen soll, was aber egal is, weil eh (4) falsch ist ... aber schauts euch das an, wer weiß, was ich um DIESE uhrzeit produziert habe ...

gute nacht dann http://hades.gothic.at/iforum/images/smilies/wink.gif

EDIT: neue datei hochgeladen, ausbesserungen siehe #6 (http://hades.gothic.at/iforum/showpost.php?p=136347&postcount=6)
EDIT2: neue datei hochgeladen, diesmal (2) und (3) bewiesen

[bosie]

i glaub du hast an fehler bei (2) und (3) gemacht! da gehört jeweils (I and notB) and ....

aber näheres siehe bitte meine pdf ... ich weiß leider net wie ich 2 und 3 ausrechnen soll, was aber egal is, weil eh (4) falsch ist ... aber schauts euch das an, wer weiß, was ich um DIESE uhrzeit produziert habe ...

gute nacht dann http://hades.gothic.at/iforum/images/smilies/wink.gif

alter bist du noch zu zeiten auf.. hast um 4 nix besseres zu tun als th. informatik? :) arm ? :D

ich geh mal pennen nach nem NETten tag ;)

[kambo]

i glaub du hast an fehler bei (2) und (3) gemacht! da gehört jeweils (I and notB) and .... dann wäre auch deine Lösung falsch http://hades.gothic.at/iforum/images/smilies/wink.gif

aha....noch was
Am Schluss hast du H1 und nicht (so wie du geschrieben hast) T1 angewendet, oder?

[ein_stein2000]

dann wäre auch deine Lösung falsch http://hades.gothic.at/iforum/images/smilies/wink.gif

aha....noch was
Am Schluss hast du H1 und nicht (so wie du geschrieben hast) T1 angewendet, oder?
ja du hast vollkommen recht, hab i beim runterkopieren von den anderen lösungen wohl net beachtet, habs jetzt ausgebessert auf H1 wie es gehört

außerdem habe ich noch einen Fehler gefunden, bei (4) ist eine doppelte verneinung wenn man einsetzt: also man hat ((I & ¬B) כ Q) wobei dann B = -atom(x) ist und wenn man einsetzt, kommt eine doppelte verneinung raus, deswegen ist (4) dann in der wahrheitstabelle richtig uns somit in S gültig (i hab auch überall in N gültig geschrieben, hab auch das ausgebessert)

dann wäre auch deine Lösung falsch http://hades.gothic.at/iforum/images/smilies/wink.gif
jo du hast recht, i hab übersehn, dass du jo mit variablen arbeitest und eben gilt B = -atom(x) und dann fehlt bei dir die Verneinung (weil die eben in B gehört) ... also passt deine lösung eh :) sry war etwas spät ...

ich hab das verbesserte file wieder oben in meinem post neu hochgeladen!

[maitscha]

zu (2) und (3): Hier erhalten wir ...

... impl. INV [build (x,y) | x]

Ergibt dann eingesetzt:

... impl. (NOT atom? (build(x,y))) OR (atom? (build(x,y)))

Einer der beiden Ausdrücke "NOT atom?" oder "atom?" sollte doch immer wahr sein, also ist der hintere Teil der Implikation wahr und die gesamt Implikation immer wahr.

Oder kann es sein dass ich da [build (x,y) | x] falsch eingesetzt habe?

[Erendis]

es wird ja auch gefragt, ob die Korrektheitsaussage stimmt, wenn man die Postcondition durch !atom?(x) ersetzt.

@ein_stein2000:
sind jetzt die 2. und 3.Formel gültig?

[ein_stein2000]

es wird ja auch gefragt, ob die Korrektheitsaussage stimmt, wenn man die Postcondition durch !atom?(x) ersetzt.

@ein_stein2000:
sind jetzt die 2. und 3.Formel gültig?
jo i hab mir nochmal (2) und (3) angeschaut ... da hab i an fehler gemacht biem einsetzen der ersetzung ... i hab jetzt auch ah lösung gefunden, siehe attachmant ... i habs wiedermal aktualisiert

[ein_stein2000]

zu (2) und (3): Hier erhalten wir ...

... impl. INV [build (x,y) | x]

Ergibt dann eingesetzt:

... impl. (NOT atom? (build(x,y))) OR (atom? (build(x,y)))

Einer der beiden Ausdrücke "NOT atom?" oder "atom?" sollte doch immer wahr sein, also ist der hintere Teil der Implikation wahr und die gesamt Implikation immer wahr.

Oder kann es sein dass ich da [build (x,y) | x] falsch eingesetzt habe?
ah jetzt seh i erst deinen post ;) und jo i hab die gleiche argumentation wie du ... sollte also passen

[r:269]

bleibt eigentlich die partielle korrektheit erhalten, wenn man die postcondition auf \neg atom?(x) ändert?

Ich bin mir dabei nicht ganz sicher, da man ja somit als Invariante (\neg atom?(x) \vee \neg atom(x)) laut script seite 105 unten wählen müsste.

Setzt man dies in (1)-(4) ein würde das bedeuten, dass auch bei änderung der postcondition die partielle korrektheitsaussage gilt ABER kann dies möglich sein, da ja die WHILE-Schleife genau dann abbricht wenn x ein Atom ist und somit die Nachbedingung atom?(x) erfüllt sein müsste?

[b_evil]

ich glaube, wenn man die postkondition auf !a(x) ändert, sollte das nichts an der partiellen korrektheit ändern, da die schleife ja weiterhin nicht terminiert, oder?