In den Prüfungsprotokollen taucht oft die Frage auf, wie die Zuweisung in den verschiedenen Semantiken formuliert ist.
Leider finde ich im Skript den Begriff Zuweisung nicht.
Was ist damit gemeint?
Zuweisung heißt im englischen "Assignment".
Edit:
Die Formel für die Zuweisung in der denotationalen Semantik lautet:
[[v:=e]]commSIGMA = [SIGMA | v:[[e]]intexpSIGMA]
Axiomatische Semantik:
__________________
{p/v |-> e} v:= e{p}
Operationale Semantik:
____________________________________________
<v:=e,SIGMA> -> [SIGMA | v:[[e]]intexpSIGMA]
wie genau funktioniert das mit der Zuweisung in axiom. Semantik?
Die Regel ist ja {p/v |-> e} v:= e{p} (wie unten beschrieben).
Wenn ich nun sage: p := x=2 und die Zuweisung ist x := 2,
wie sieht dann die Vorbedinung aus? Ich soll ja überall,
wo in der Vorbedingung x steht, dies durch 2 ersetzen.
Wäre das dann {2=2} x:= 2 {x=2} ?
Und wie sieht das dann aus, wenn ich folgendes schließen will:
{x = 42} x:= 23 {x=23}? Dann erweitere ich vielleicht die
Vorbedingung wieder zu {x = 42, 23=23}, aber das Problem ist,
dass dann die Nachbedingung doch heißen könnte:
{x = 42, x = 23} = {false}
Spezifikation: {x=42} x:= 23 {x=23}
1. Schritt
{23=23} x:= 23 {x=23}
darst du dir ausdenken (Axiom),
2. Schritt
und danach verstärken
{x=42} x:= 23 {x=23}
da x=42 -> 23=23
damit ist {x=42} x:= 23 {x=23} erfolgreich abgeleitet,
———-
die Nachbedigung kannst du nicht einfach zu false verstärken, dazu gibt es keine Regel
falls du dir vorgenommen hast {x=42} x:= 23 {false} nachzuweisen,
dann wirst du scheitern, da dies ja nicht part. korrekt ist
danke, ich denke das hab ich verstanden.
Mein Problem war, dass die Regel zwar besagt,
dass aus der Vorbedingung
{23=23} durch x:=23 {x=23} werden darf,
aber es stand nirgendwo etwas, dass zusätzliche
Vorbedingungen wie eben x=42 dadurch entwertet
werden und nacher nicht mehr gelten. Das hatte
mich ein wenig verwirrt. Aber wenn man das so
in den 2 Schritten sieht, ist es ok
