Herleitung im Hoare-Kalkül < Logik < Logik+Mengenlehre < Hochschule < Mathe < Vorhilfe
|
| Aufgabe | | Es handelt sich nicht um eine Übungsaufgabe. |
Hallo ihr,
als wir in einer Vorlesung das Hoare-Kalkül durchgenommen haben, haben wir die negativen Auswirkungen der Undefiniertheiten von Termen am Beispiel der Hoare-Formel
[mm] \{true\} [/mm] x := 1 div 0 [mm] \{false\}
[/mm]
verdeutlicht. Wir haben festgestellt, dass die Formel gültig ist, da die Semantik von [mm] \{true\} [/mm] x := 1 div 0 [mm] \{false\} [/mm] angewendet auf den Speicher [mm] \sigma [/mm] ungleich [mm] \perp [/mm] für [mm] \sigma \not= \perp [/mm] ist (und somit die Hoare-Formel falsch ist), aber sie nicht im Hoare-Kalkül hergeleitet werden kann, da es keine Gültigkeit von true [mm] \to [/mm] false gibt.
Ich möchte zu [mm] \{true\} [/mm] x := 1 div 0 [mm] \{false\} [/mm] die Herleitung aufstellen um zu verifizieren, dass wir wirklich das Problem true [mm] \to [/mm] false haben. Doch wie stelle ich den Herleitungsbaum auf? Der Anfang ist klar, also
[mm] \overline{ \{true\}\ x \: =\ 1\ div\ 0\ \{false\} }
[/mm]
Jetzt müsste das Zuweisungsaxiom angewendet werden. Das ist definiert durch [mm] \{\phi[t/x]\} [/mm] x := [mm] t\{\phi\}. [/mm] Leider weiß ich nicht, wie ich es anwenden soll.
Liebe Grüße
kraulquappe
Ich habe diese Frage in keinem Forum auf anderen Internetseiten gestellt.
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig  | | Datum: | 16:20 So 17.02.2013 | | Autor: | matux |
$MATUXTEXT(ueberfaellige_frage)
|
|
|
|
