Denotationale Semantik

aus Wikipedia, der freien Enzyklopädie

Du hast neue Nachrichten auf deiner Diskussionsseite.

Die Denotationale Semantik der Informatik (Funktionensemantik) beschreibt die Wirkungsweise eines Programms als partielle Abbildung eines Speicherzustandes in einen anderen. Die Regeln des Kalküls legen (induktiv) fest, wie die Funktion zu einem Programm gebildet wird.

[Bearbeiten] Definition der semantischen Funktion $\ f$

Sei $\mathcal{Z}$ die Menge aller möglichen Speicherzustände. Die Wirkung, die eine Anweisung $\ A$ auf einen Zustand hat, ist formal gesprochen eine Abbildung

$f[A]:\mathcal{Z}\rightarrow\mathcal{Z}$ ,

die einem Zustand $z\in\mathcal{Z}$ einen Folgezustand $z'\in\mathcal{Z}$ zuordnet.

$\ f$ bezeichnet die semantische Funktion und ordnet jedem Anweisungskonstrukt eine Bedeutung zu, indem sie eine Zustandsänderung des Programms bewirkt.

Nachfolgend wird die Wirkung der wichtigsten Kontrollstrukturen einer Programmiersprache auf einen Speicherzustand untersucht.

Die Bedeutung der leeren Anweisung $\ null$ :

$f[null](z)\ =\ z$ .

Die leere Anweisung, angewendet auf einen Zustand $\ z$ , verändert den Zustand nicht.

Die Semantik einer Anweisungsfolge kann folgendermaßen beschrieben werden:

$f[A_1,A_2](z)\ =\ f[A_2](f[A_1](z))$ .

Die Bedeutung dieser Befehlssequenz, ist die Wirkung von $\ A_2$ angewendet auf den Zustand, der sich ergibt nachdem $\ A_1$ auf $\ z$ ausgeführt wurde.

Für die Wirkung einer Zuweisung auf einen Speicherzustand gilt:

$f[x:=E](z)\ =\ \begin{cases} \perp, &wenn\ [E](z)=\perp \\ z', &sonst \end{cases}$ .

Das Programm terminiert nicht ( $\ \perp$ ), wenn die Anweisung (oder der Ausdruck) $\ [E]$ angewendet auf Zustand $\ z$ nicht terminiert. In allen anderen Fällen geht das Programm in einen Zustand $\ z'$ über.

Für die zwei-seitige Alternative gilt:

$f[if\ B\ then\ C_1\ else\ C_2](z)= \begin{cases} f[C_1](z), & wenn\ B[z] = true \\ f[C_2](z), & wenn\ B[z]=false \\ \perp, &sonst \end{cases}$ .

Der Folgezustand entspricht $\ [C_1]$ angewendet auf $\ z$ , wenn $\ B[z]=true$ . Wenn $\ B[z]=false$ so wird der nachfolgende Zustand durch $\ [C_2]$ angewendet auf $\ z$ bestimmt. In allen anderen Fällen terminiert das Programm nicht.

Die Bedeutung der Wiederholung definiert sich rekursiv zu:

$f[while\ B\ do\ L](z)=\begin{cases} z, &wenn\ [B](z)=false \\ \perp, &wenn\ [B](z)=\perp\ \or\ [L](z)=\perp \\ f[while\ B\ do\ L]([L](z)), &sonst\end{cases}$ .

Falls $\ [B](z)=false$ so bewirkt die While-Anweisung keine Zustandsänderung.

Wenn $\ [B](z)=\perp$ oder $\ [L](z)=\perp$ so terminiert das gesamte Programm nicht.

In allen anderen Fällen wird erneut die Wiederholungsanweisung $\ [while\ B\ do\ L]$ auf den Zustand der sich nach Ausführung von $\ [L](z)$ ergibt, angewendet.

Durch diese rekursive Definition kann man nicht auf die Wirkung dieser Anweisung schließen. Man ist daher an dem Fixpunkt der While-Schleife interessiert.

[Bearbeiten] Fixpunkt der While-Semantik

Der Fixpunkt der While-Schleife wird nachfolgend anhand eines einfachen Beispiels erläutert.

$\ while\ x\not=y\ do\ y:=y+1$

Solange x ungleich y wird der Wert der Variablen y um 1 erhöht.

Um den Fixpunkt dieser Gleichung zu bestimmen, bedient man sich des Tarskischen Fixpunktsatzes.

Dieser Satz besagt, dass für eine geordnete Menge $\ \mathcal{M}$ , welche ein kleinstes Element besitzt, und eine streng monotone Funktion, welche M auf sich selbst abbildet, ein kleinster Fixpunkt existiert.

Damit der Satz angewendet werden kann, muss zuerst eine geordnete Menge für das Beispiel definiert werden.

Sei $w:(\mathbb{Z}\times\mathbb{Z})\rightarrow(\mathbb{Z}\times\mathbb{Z})$ die partielle Funktion der While Schleife aus dem Beispiel. Diese bildet einen Speicherzustand, bestehend aus der Belegung für die Variablen (x,y) in einen anderen Speicherzustand mit der Variablenbelegung (x',y') ab. Die Variablen x und y sind dabei ganze Zahlen.

Sei nun $\mathcal{P}_{(\mathbb{Z}\times\mathbb{Z})}$ die Menge aller partiellen Funktionen $\ w$ .

Die partielle Ordnung $\sqsubseteq$ für zwei partielle Funktion $\ w$ , $\ w' \in \mathcal{P}_{(\mathbb{Z}\times\mathbb{Z})}$ sei wie folgt definiert:

$\ w \sqsubseteq w' \Leftrightarrow \ dom(w) \subseteq dom(w') \wedge w(x,y)=(x',y') \rightarrow w'(x,y)=(x',y')$ .

Die partielle Abbildung $\ w$ ist kleiner als $\ w'$ genau dann, wenn der Definitionsbereich von $\ w$ eine echte Teilmenge des Definitionsbereichs von $\ w'$ ist. Zudem muss gelten, dass wenn $\ w(x,y)$ eine Zustandsänderung nach $\ (x',y')$ bewirkt, so muss auch Funktion $\ w'(x,y)$ in $\ (x',y')$ abbilden.

Das kleinste Element der Menge $\mathcal{P}_{(\mathbb{Z}\times\mathbb{Z})}$ sei die nirgends definierte Funktion $\perp$ .

Um den Satz von Tarski verwenden zu können, fehlt nun noch eine streng monotone Funktion, die $\mathcal{P}_{(\mathbb{Z}\times\mathbb{Z})}$ auf sich selbst abbildet. Dazu wird eine Funktion $\ f$ definiert:

$\ f:\mathcal{P}_{(\mathbb{Z}\times\mathbb{Z})}\rightarrow \mathcal{P}_{(\mathbb{Z}\times\mathbb{Z})}$ .

Laut obigen Beispiel gilt für $\ f$ :

$\ f(w)(x,y)=\begin{cases}(x,y), &wenn\ x=y \\ w(x,y+1), &sonst \end{cases}$ .

Weiterhin sei:

$\ w_{n+1}=f(w_n)\ \forall n\isin\mathbb{N}$ .

Nun sind alle Voraussetzungen des Fixpunktsatzes erfüllt, es existiert ein Fixpunkt.

Den Fixpunkt berechnet man durch Grenzwertbildung der Funktion $\ f$ .

Um auf den Grenzwert schließen zu können, beginnt man mit dem Ausrechnen einzelner Funktionswerte.

$\ w_0(x,y)= \perp$ , da $\ w_0$ das kleinste Element der Menge $\mathcal{P}_{(\mathbb{Z}\times\mathbb{Z})}$ ist.

$\ w_1(x,y)$ ist laut Definition der Funktion $\ f$ :

$\ w_1(x,y)=f(w_0)(x,y)=\begin{cases}(x,y),&wenn\ x=y \\ w_0(x,y+1)=\perp,&sonst\end{cases}$ .

$\ w_2(x,y)$ ergibt sich zu:

$\ w_2(x,y)=f(w_1)(x,y)=\begin{cases}(x,y),&wenn\ x=y \\ w_1(x,y+1)=\begin{cases}(x,y+1),&wenn\ x=y+1 \\ \perp,&sonst \end{cases}\end{cases}$ .

Für $\ w_n$ kann formuliert werden:

$\ w_n(x,y)=f(w_{n-1})(x,y)=\begin{cases}(x,x),&wenn\ x-(n-1) \le y \le x \\ \perp,& sonst\end{cases}$ .

Der Grenzwert $\ w_{\infty} = w_n \ \forall \ n \isin \mathbb{N}$ sei nun:

$w_{\infty}(x,y)=\begin{cases}(x,x),&wenn\ -\infty \le y \le x \\ \perp,& sonst\end{cases}$ .

Für den Fixpunkt muss nun gelten, dass $\ f(w_{\infty})(x,y)=w_{\infty}(x,y)$ .

$\ f(w_{\infty})(x,y)=\begin{cases}(x,y),&wenn \ x=y \\ w_{\infty}(x,y+1)= \begin{cases}(x,x), &wenn\ -\infty \le y < x \\ \perp,&sonst\end{cases}\end{cases}$ .

Dies kann umgeformt werden zu:

$\ f(w_{\infty})(x,y)=\begin{cases}(x,x), &wenn\ -\infty \le y \le x \\ \perp,&sonst\end{cases}$ .

Somit gilt $\ f(w_{\infty})(x,y)=w_{\infty}(x,y)$ . Der Fixpunkt ist gefunden. Die Bedeutung der While-Schleife aus dem Beispiel ergibt sich aus dem Fixpunkt. Die Schleife terminiert, wenn $\ y \le x$ und liefert das Tupel $\ (x,x)$ . Falls $\ y > x$ so terminiert die Schleife nicht.