Zuweisungsregel

Jetzt können wir in Q’ jede gestrichene Variable wieder

heraussubstituieren:

P Þ Q’ [v’ ® v, x’ ® t]

{ P } x := t { Q }

v’ = v

x’ = t

Für jede Variable ¹ x

Vorherige Folie

Nächste Folie

Zurück zur ersten Folie

Graphik-Version anzeigen