hoare kalkül, seite 106

[reddi]

hallo!

ich habe zum hoare kalkül zwei fragen ;-)

auf seite 106 oben ist eine erläuterung, wie man die invariante für while-schleifen wählt! ich kann mich erinnern, dass fermüller hier eine anschauliche erklärung gebracht hat, warum die invariante genau so gewählt wird

und die zweite frage ist folgende:
ganz unten muss die gültigkeit der formel (1) bewiesen werden (ist mir klar)
nur blick ich nicht ganz durch, wieso y < x+y ist und die zeilen darunter! die erste zeile ist mir klar (da hat er P,Q und B zurücksubstituiert), aber ab hier sind einige sachen unklar!


wäre nett, wenn sich jemand finden könnte, der hier ein paar kurze - va. helfende - worte verlieren könnte

[tobias]

Zur zweiten Frage (Angaben wie links/rechts sind relativ zur Implikation):
t impliziert f darf nicht möglich sein, da die Formel sonst widerlegbar ist
1) y < x+y, da x=3 (x muss 3 sein, damit die linke Seite t ist)
2) x+y < 19 (muss gelten, damit die linke Seite t ist)
3) 19 < x+19 => 19 < 22
4) y < x+y < 19 < x+19 => y < x+19

Diese Variante ist zwar elegant, intuitiver finde ich aber folgendes:
Ich versuche zu zeigen, dass die Formel widerlegbar ist, also t impliziert f möglich ist
Damit die linke Seite t wird muss gelten: x=3 und x+y < 19 also y < 16
Mit y < 16 erhalten wir auf der rechten Seite (y < 22) immer eine wahre Aussage. Die Formel ist damit nicht widerlegbar und gültig.

Tobias

[reddi]

Zur zweiten Frage (Angaben wie links/rechts sind relativ zur Implikation):
t impliziert f darf nicht möglich sein, da die Formel sonst widerlegbar ist
1) y < x+y, da x=3 (x muss 3 sein, damit die linke Seite t ist)
2) x+y < 19 (muss gelten, damit die linke Seite t ist)
3) 19 < x+19 => 19 < 22
4) y < x+y < 19 < x+19 => y < x+19

Diese Variante ist zwar elegant, intuitiver finde ich aber folgendes:
Ich versuche zu zeigen, dass die Formel widerlegbar ist, also t impliziert f möglich ist
Damit die linke Seite t wird muss gelten: x=3 und x+y < 19 also y < 16
Mit y < 16 erhalten wir auf der rechten Seite: y < 16 < 22
Das stimmt natürlich nicht und damit ist die Formel nicht widerlegbar.

Tobias

danke, wenn deine lösung korrekt ist, versteh ich das endlich ;-) und werde das auch so machen wie du es gemacht hast im falle das soetwas zur prüfung kommt! trotzdem wäre interessant, wieso die annahme:
y<x+y
getroffen wurde

reine intuition? ich meine wenn x gleich 3 ist ist schon klar, dass die ungleichung erfüllt ist, aber wieso kommt er auf diesen ansatz? meine vermutung ist ja, dass er von der linken seite auf einen term ala y<x+19 kommen will und somit gleich sagen kann: t impliziert t --> nicht widerlegbar!

[Septic.exe]

Mit y < 16 erhalten wir auf der rechten Seite: y < 16 < 22
Das stimmt natürlich nicht und damit ist die Formel nicht widerlegbar.

Klar stimmt das, es ist aber so nicht möglich, die rechte Seite auf "f" zu führen ... oder?

[tobias]

Klar stimmt das, es ist aber so nicht möglich, die rechte Seite auf "f" zu führen ... oder?

Äh, ja. Danke für den Hinweis, ich bessere es oben noch aus.

Tobias

[Septic.exe]

War keine Kritik, nur 'ne Anmerkung. Ohne Deine Erklärung würd' ich immer noch davor sitzen und mir auf'n Kopf greifen *g* ;).

[owaye]

HOARE the WHORE! :D

[maitscha]

Ich hätte zum Hoare-Kalkül noch folgende Frage:

Ich bin an einem Ast und hab folgenden Ausdruck stehen:

INV {z <- z+x} Q [x+z x]

Nun wende ich H1 an. Wie sieht nun die Reihenfolge der zwei Ersetzungen aus? INV impl. Q [x+z x] [z+x z] oder INV impl. Q [z+x z] [x+z x] ? Oder spielt es keine Rolle in welcher Reihenfolge ich die anschreibe?

[Dieli]

Ich hätte zum Hoare-Kalkül noch folgende Frage:

Ich bin an einem Ast und hab folgenden Ausdruck stehen:

INV {z <- z+x} Q [x+z x]

Nun wende ich H1 an. Wie sieht nun die Reihenfolge der zwei Ersetzungen aus? INV impl. Q [x+z x] [z+x z] oder INV impl. Q [z+x z] [x+z x] ? Oder spielt es keine Rolle in welcher Reihenfolge ich die anschreibe?
Hätte gesagt, Q[x+z x] [z+x z], da die Regel ja sagt, dass du dein R von vorher (Q [x+z x]) nimmst und hinten das neue schreibst. Ganz sicher bin ich mir aber auch nicht.

mfg Dieli