Ausdrücke

Ausdrücke entsprechen im Wesentlichen den Termen einer funktionalen/logischen Sprache, jedoch stehen an der Stelle von Unbestimmten nun Variablen. Die Auswertung von Termen ist zustandsabhängig:

Gegebener Term:   $2\cdot X+1$ 
Wert im Zustand Z ist durch  $2\cdot Z(X)+1$  bestimmt

Wert eines Ausdrucks

Der Wert eines Ausdrucks $t(X_{1},...,X_{n})$ wird mit $Z(t(X_{1},...,X_{n}))$ bezeichnet:

 $Z(2\cdot X+1)=2\cdot Z(X)+1$

Damit ist auch die Wertzuweisung mit Variablen möglich

 $X:=t(X_{1},...,X_{n})$

Der Transformierte Zustand ist definiert als:

 $[\![X:=t(X_{1},...,X_{n})]\!](Z)=Z\langle X\leftarrow Z(t(X_{1},...,X_{n}))\rangle$

Den Zustand liest man so, dass X dem Wert des Ausdrucks $t(X_{1},...,X_{n})$ zugeordnet wird. Die Semantikklammern bedeuten, dass eine Anweisung als eine Funktion auf Zuständen definiert ist.

Literatur

Da die Vorlesungsinhalte auf dem Buch Algorithmen und Datenstrukturen: Eine Einführung mit Java von Gunter Saake und Kai-Uwe Sattler aufbauen, empfiehlt sich dieses Buch um das hier vorgestellte Wissen zu vertiefen. Die auf dieser Seite behandelten Inhalte sind in Kapitel 3.3.1 zu finden.