Formale Semantik

Hartwig, Rolf

Teilnehmerkreis:

Obligatorisch für Informatikstudenten und Magisterstudenten mit Hauptfach Informatik im Hauptstudium, wahlobligatorisch und empfohlen für alle Studenten mit Nebenfach Informatik

Übersicht:

In der Vorlesung werden verschiedene Methoden der Semantikdefinition von Programmiersprachen gegenübergestellt. Je nach dem Ziel der formalen Semantikbeschreibung sind unterschiedliche Methoden zweckmäßig. Ausführlich werden die operationale Methode und die denotationale Methode der Semantikdefinition behandelt. Weitere Methoden wie z.B. die algebraische Semantik oder die axiomatische Semantik werden nur im Ansatz vorgestellt. Sie sind Gegenstand anderer Vorlesungen (u.a. desselben Lesenden in evtl. auch anderen Semestern).

Gliederung:

1. Einführung
   • Syntax, Semantik und Pragmatik von Programmiersprachen
   • Methoden der Semantikdefinition
2. Operationale Methode
   • Eine abstrakte Maschine
   • Semantikdefinition für eine Beispielsprache
   • Semantik eines Beispielprogramms
3. Denotationale Semantik
   • Syntaktische und semantische Bereiche
   • Fixpunktgleichungen
   • Vollständige Halbordnungen und Fixpunktsatz
   • Vollständige Halbordnungen und denotationale Semantik

Literatur:

• de Bakker, J.W.: Mathematical Theory of Program Correctness, Prentice Hall Int. 1980
• Fehr, E.: Semantik von Programmiersprachen, Springer, 1989
• Riedewald, G. u.a.: Formale Beschreibung von Programmiersprachen, Berlin, 1983

Erwartete Vorkenntnisse:

Kenntnis einer höheren Programmiersprache, mengentheoretisch-algebraische Grundkenntnisse

Scheinvergabe:

Bei regelmäßigem Vorlesungsbesuch, evtl. abschließendes Einzelgespräch (Testat)

Sonstiges:

Zur Vorlesung gibt es eine überarbeitete studentische Mitschrift als Vorlesungsskript.