Es gibt verschiedene Ansätze die Semantik einer Programmiersprache und ihr Typsystem zu beschreiben. Wir werden drei-einhalb Beschreibungstypen kennenlernen und die sogenannten Operationalen Semantiken am Beispiel einer einfachen Sprache näher erklären. Operationale Semantiken werden uns in den folgenden Kapiteln immer begleiten.
Übersetzersemantik:
Beschreibt die Semantik einer Programmiersprache durch
Übersetzungsregeln in eine andere Programmiersprache mit bereits
bekannter Semantik. Diese Beschreibungsart ist somit nicht vollkommen
eigenständig, sondern bedingt immer das es bereits eine Beschreibung
für irgendeine andere Sprache gibt. Sie ist allerdings nützlich,
wenn wir zum Beispiel eine realistische Programmiersprache mit Hilfe
von einigen Übersetzungregeln auf ihren Kern reduzieren wollen.
So könnte man zum Beispiel eine Übersetzersemantik für die Sprache
C erfinden, die sämtliche for-Schleifen in
while-Schleifen überführt und if-Anweisungen
ohne else-Teil um einen leeren else-Teil
ergänzt um so eine einfachere Kernsprache zu erhalten.
Operationale Semantik (Interpretersemantik):
Beschreibung der Semantik einer Programmiersprache mit Hilfe von
schrittweisen Verarbeitungsregeln für Terme dieser Sprache. Wird im nächsten
Teil genauer betrachtet.
Denotationale Semantik (Funktionensemantik):
Beschreibt die Semantik einer Anweisung mit Hilfe einer
Abbildungsfunktion (F[a] : Z → Z), die einer Anweisung a
eine Transformation des Programmzustands auf den Folgezustand zuordnet.
Beispiel: F[x:=y+1] (1,3) = (4,3)
Axiomatische Semantik (Pradikatensemantik):
Ist die abstrakteste der betrachteten Beschreibungsformen. Sie beschreibt die
Semantik von Konstrukten einer Sprache mit Hilfe von Vor-
und Nachbedingungen ({P}a{Q}), ohne dabei anzugeben, wie die Transformation
des Programmzustands erfolgt. Beispiel: {x>=1} x:=x-1 {x>=0}
Wir wollen nun eine einfache Sprache für Boolsche Ausdrücke betrachten.
Die Sprache sei durch die folgende abstrakte Syntax beschrieben:
|
Abstrakte Syntax, im Gegensatz zu konkreter Syntax, meint hier zum Beispiel dass wir in konkreten Ausdrücken durchaus Klammern zur besseren Lesbarkeit (eine andere Funktion haben sie in dieser Sprache nicht) verwenden dürfen. Die Klammern sind aber nicht Bestandteil der abstrakten Syntax. Dort wird davon ausgegangen, dass wir bereits einen eindeutigen Programmbaum vorliegen haben.
Konkrete Ausdrücke in unserer Sprache sind beispielsweise:
|
Betrachten wir nun die Semantik dieser Sprache anhand einer operationalen Semantik:
Ein Teilmenge aller Terme haben wir als Werte definiert. Werte sind spezielle
Terme, die sich nicht weiter vereinfachen lassen. Die Auswertung (→) eines
Terms beschreiben wir mit Hilfe von zwei sogenannten Axiomen (das sind Regeln
ohne Prämisse) und einer Regel mit Prämisse. Axiom (1) besagt, dass if true then
t2 else t3 jederzeit (für alle Terme t2 und t3) zu
t2 ausgewertet werden kann. Axiom (2) besagt entsprechend, dass
if false then t2 else t3 jederzeit zu t3 ausgewertet
werden kann. Die Regel (3) besagt schliesslich, dass wenn der Term t1 zu
t1' ausgewertet werden kann auch der Term if t1 then t2 else t3
zu if t1' then t2 else t3 ausgewertet werden kann.
In einem konkreten Beispiel würde die folgende Auswertung stattfinden:
|
Zunächst wird mit der Regel (3) der Teilausdruck (if false then true else false)
zur weiteren Verabeitung ausgewählt und mit Axiom (2) zu false ausgewertet.
Danach wird der äußere Ausdruck mit Axiom (2) zu
if true then false else true ausgewertet. Dieser Ausdruck wird dann mit
Axiom (1) zu false ausgewertet. Auf diesen Ausdruck läßt sich keine
Auswertungsregel mehr anwenden. Ein Term der nicht weiter vereinfacht werden
kann wird als Term in Normalform bezeichnet.
Für unsere Sprache gelten die folgenden Eigenschaften:
Werte sind in Terme in Normalform:
Auf einen Wert trifft nie irgendeine Auswertungsregel zu. Diese Eigenschaft
ist praktisch schon ein definitorisches Kriterium. Jede Sprache die diese
Eigenschaft nicht hat, ist kaputt. In unserem Beispiel wäre es
ziemlich schlimm, wenn wir beispielsweise aus true false
ableiten könnten.
Jeder Term in Normalform ist ein Wert:
Läßt sich ein Term nicht weiter vereinfachen, handelt es sich um einen Wert, in
unserem Fall um true oder false. Wir werden Sprachen
kennen lernen in denen nicht jeder Term in Normalform ein Wert ist, sondern
auch die Möglichkeit besteht, dass es sich bei einem Term in Normalform
um einen Fehlerterm handelt, der einen Laufzeitfehler (zum Beispiel eine
Exception) repräsentiert.
Die Auswertung (→) erfolgt deterministisch:
Auf keinen Term läßt sich mehr als eine Auswertungsregel anwenden. In unserem Beispiel
könnten wir zum Beispiel nicht zuerst den Teilterm (if true then false else true)
auswerten. Es ist nur diese eine Auswertungsreihenfolge möglich. Diese Eigenschaft
gilt nicht für jede Sprache. Ein prominentes Beispiel ist die Programmiersprache C in
der die Auswertungsreihenfolge von Funktionsargumenten undefiniert ist.
Jeder Term hat eine Normalform:
Jeder Term dieser Sprache kann nach einer endlichen Folge von Schritten in eine Normalform
überführt werden. Man könnte auch sagen jedes Programm in unserer Sprache terminiert.
Programmiersprachen haben diese Eigenschaft in der Regel nicht. In jeder Sprache die mächtig
genug ist um eine universelle Turingmaschine zu simulieren, gibt es zwangsläufig
auch Programme die nicht terminieren.
Steuerung der Auswertungsreihenfolge
In der oben angegebenden operationalen Semantik gilt die folgende Auswertungsreihenfolge:
Es wird zunächst die Bedingung ausgewertet und danach abhängig von der Normalform der
Bedingung entweder der
Die folgende operationale Semantik erzwingt eine andere Auswertungsreihenfolge:
In dieser operationalen Semantik wurden an einigen Stellen die Metavariablen
t1, t2 und t3, die für beliebige Terme stehen, durch die Metavariablen v1, v2 und v3,
die für Werte (values) stehen, ausgetauscht. Dadurch, dass wir an einigen Stellen
Werte gefordert haben, haben wir die folgende Auswertungsreihenfolge erzwungen:
Es wird zunächst der
Unten haben wir nochmal den bereits bekannten Term
Die Implementierung in Haskell entspricht praktisch direkt unserer ursprünglichen operationalen
Semantik. Terme werden durch den Datentyp
Einzig gewöhnungsbedürftigt ist die neue Notation für Terme so steht
Ein konkrete Session im ghci könnte wie folgt aussehen (Benutzereingaben kursiv):
then-Term oder der else-Term. Dies entspricht
der üblichen Semantik von bedingten Ausdrücken in Programmiersprachen. Wir können aber
auch jede beliebige Auswertungsreihenfolge erzwingen, ohne dabei die oben genannten
Eigenschaften, insbesondere Determinismus, zu gefährden.
then-Term, dann der else-Term, dann
erst die Bedingung ausgewertet, erst dann kann eines der Axiome (1') oder (2') angewendet
werden.
if (if false then true else false) then true else (if true then false else true)
nach den neuen Auswertungsregeln ausgewertet. Es ist dabei nur die folgende Reihenfolge
möglich : Regel (5), Axiom (1'), Regel (3'), Axiom (1'), Axiom (2'):
if (if false then true else false) then true else (if true then false else true)
-> if (if false then true else false) then true else (if true then false else true)
-> if (if false then true else false) then true else false
-> if (if false then true else false) then true else false
-> if false then true else false
-> false
Implementierung in Haskell
module B (Term,eval)
where
data Term = TmTrue | TmFalse | TmIf Term Term Term
deriving Show
eval :: Term -> Term
eval (TmIf TmTrue t2 _ ) = eval t2 -- Axiom 1
eval (TmIf TmFalse _ t3) = eval t3 -- Axiom 2
eval (TmIf t1 t2 t3) = eval (TmIf (eval t1) t2 t3) -- Regel 3
eval t = t -- Normalform
Term repräsentiert. Term hat die
Typkonstruktoren TmTrue, TmFalse und TmIf Term Term Term.
Die Auswertungsfunktion (→) haben wir eval genannt.
TmIf TmFalse TmTrue TmTrue für den Term if false then true else true.
Dies ist aber nicht problematisch, da wir uns mit der abstrakten Syntax von Termen und nicht mit
ihrer konkreten Syntax befassen. Wir gehen also hier davon aus, dass uns bereits ein
Programmbaum vorliegt. Wie man von einer konkreten Syntax zu einem Programmbaum kommt
ist Gegenstand der Vorlesung Compilerbau und soll uns an dieser Stelle nicht weiter
interessieren.
Prelude> :load b
Compiling B ( b.hs, interpreted )
Ok, modules loaded: B.
*B> eval (TmIf (TmIf TmFalse TmTrue TmFalse) TmTrue (TmIf TmTrue TmFalse TmTrue))
TmFalse
*B>