Denotationelle Semantik

Metasprache zur Definition einer formalen Semantik

Die denotationelle Semantik (Funktionensemantik; englisch: denotational semantics) ist in der Theoretischen Informatik eine von mehreren Möglichkeiten, eine formale Semantik für eine formale Sprache zu definieren. Die formale Sprache dient hierbei als mathematisches Modell für eine echte Programmiersprache. Somit kann die Wirkungsweise eines Computerprogramms formal beschrieben werden.

Konkret kann man etwa bei einer gegebenen Belegung für Eingabevariablen das Endergebnis für eine Menge von Ausgabevariablen mit der denotationellen Semantik berechnen. Es sind auch allgemeinere Korrektheitsbeweise möglich.

Bei der denotationellen Semantik werden partielle Funktionen verwendet, die Zustandsräume aufeinander abbilden. Ein Zustand ist hier eine Belegung von Variablen mit konkreten Werten. Die denotationelle Semantik wird induktiv über die syntaktischen Anweisungskonstrukte der formalen Sprache definiert. Abhängig von der gewünschten Programmsemantik werden die partiellen Funktionen gewählt.

Neben der denotationellen Semantik gibt es auch die operationelle Semantik und die axiomatische Semantik, um die Semantik von formalen Sprachen zu beschreiben.

Definition der semantischen Funktion f

Bearbeiten

Sei   die Menge aller möglichen Zustände. Die Wirkung, die eine Anweisung   auf einen Zustand hat, ist formal gesprochen eine Abbildung

 ,

die einem Zustand   einen Folgezustand   zuordnet.

  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 Zustand untersucht.

  • Die Bedeutung der leeren Anweisung  :
 .
Die leere Anweisung, angewendet auf einen Zustand  , verändert den Zustand nicht.
  • Die Semantik einer Anweisungsfolge kann folgendermaßen beschrieben werden:
 .
Die Bedeutung dieser Befehlssequenz ist die Wirkung von   angewendet auf den Zustand, der sich ergibt, nachdem   auf   ausgeführt wurde.
  • Für die Wirkung einer Zuweisung auf einen Zustand gilt:
 
Das Programm terminiert nicht ( ), wenn die Anweisung (oder der Ausdruck)   angewendet auf Zustand   nicht terminiert. In allen anderen Fällen geht das Programm in einen Zustand   über.
  • Für die zwei-seitige Alternative gilt:
 .
Der Folgezustand entspricht   angewendet auf  , wenn  . Wenn  , so wird der nachfolgende Zustand durch   angewendet auf   bestimmt. In allen anderen Fällen terminiert das Programm nicht.
  • Die Bedeutung der Wiederholung definiert sich rekursiv zu:
 .
Falls  , so bewirkt die While-Anweisung keine Zustandsänderung.
Wenn   oder  , so terminiert das gesamte Programm nicht.
In allen anderen Fällen wird erneut die Wiederholungsanweisung   auf den Zustand angewendet, der sich nach Ausführung von   ergibt.
Durch diese rekursive Definition kann man nicht auf die Wirkung dieser Anweisung schließen. Man ist daher am Fixpunkt der Funktion interessiert, der die Semantik der While-Schleife beschreibt.

Fixpunkt der While-Semantik

Bearbeiten

Der Fixpunkt der Funktion, die die Semantik der While-Schleife beschreibt, wird nachfolgend anhand eines einfachen Beispiels erläutert.

 
Solange   ungleich  , wird der Wert der Variablen   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  , welche ein kleinstes Element besitzt, und eine streng monotone Funktion, welche   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   die partielle Funktion der While-Schleife aus dem Beispiel. Diese bildet einen Zustand, bestehend aus der Belegung   für die gleichnamigen Variablen, in einen anderen Zustand mit der Variablenbelegung   ab. Die Variablen   und   sind dabei ganzzahlig.

Sei nun   die Menge aller partiellen Funktionen  .

Die partielle Ordnung   für zwei partielle Funktionen  ,   sei wie folgt definiert:

 .

Die partielle Abbildung   ist kleiner/gleich   genau dann, wenn der Definitionsbereich von   eine Teilmenge des Definitionsbereichs von   ist. Zudem muss gelten, dass wenn   eine Zustandsänderung nach   bewirkt, auch Funktion   nach   abbildet.

Das kleinste Element der Menge   ist die nirgends definierte Funktion  .

Um den Satz von Tarski verwenden zu können, fehlt nun noch eine streng monotone Funktion, die   auf sich selbst abbildet. Dazu wird eine Funktion   definiert:

 .

Laut obigen Beispiel gilt für  :

 .

Weiterhin sei:

 .

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

Den Fixpunkt berechnet man durch Grenzwertbildung der Funktion  .

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

  •  , da   das kleinste Element der Menge   ist.
  •   ist laut Definition der Funktion  :
 .
  •   ergibt sich zu:
 .
  • Für   kann formuliert werden:
 .

Der Grenzwert   sei nun:

 .

Für den Fixpunkt muss nun gelten, dass  .

 .

Dies kann umgeformt werden zu:

 .

Somit gilt  . Der Fixpunkt ist gefunden. Die Bedeutung der While-Schleife aus dem Beispiel ergibt sich aus dem Fixpunkt. Die Schleife terminiert, wenn  , und liefert das Tupel  . Falls  , so terminiert die Schleife nicht.

Literatur

Bearbeiten