Semantik von Programmiersprachen (SS 99)

Reinhold Heckmann

Theoretische Stammvorlesung für Hörer mit Vordiplom

Vorlesung: Dienstag, Donnerstag 14-16, Hörsaal 003 (Bau 45) (Reinhold Heckmann)
Übungen: Montag 16-18, SR 014 (Bau 45) (Tim Priesnitz)
Mittwoch 14-16, SR 014 (Bau 45) (Tim Priesnitz)

Voraussetzungen zur Scheinvergabe:
Die Hälfte der Punkte aus den Übungen (eventuell auch weniger) plus Bestehen einer Abschlußklausur

Klausur: Dienstag, 20. Juli, 10.00st-12.00, Hörsaal 003 (Bau 45)
Erlaubte Hilfsmittel: Skripten, Bücher
Klausur    Ergebnisse der Klausur

Nachklausur:  Mittwoch, 25. August, ab 10.00st, Hörsaal 003 (Bau 45)
Nachklausur    Ergebnisse der Nachklausur
Klausureinsicht:  Dienstag, 31. August, 16.00st, Raum 403, Bau 45

Die Scheine können im Sekretariat von Herrn Prof. Wilhelm abgeholt werden (Frau Günther, Zimmer 408, Bau 45). Das Sekretariat ist vormittags geöffnet, außer wenn Frau Günther Urlaub hat.

Alte Klausuren vom SS 1998 (Heckmann):
Probeklausur    Hauptklausur    Nachklausur
Beachten Sie, daß damals manches etwas anders präsentiert worden ist.

Übungen:
Übung 1 (ps.gz) (Abgabe 22. April)
Übung 2 (ps.gz) (Abgabe 29. April)
Übung 3 (ps.gz) (Abgabe 6. Mai)
Übung 4 (ps.gz) (Abgabe bis 14. Mai)
Übung 5 (ps.gz) (Abgabe 20. Mai)
Übung 6 (ps.gz) (Abgabe 27. Mai)
Übung 7 (ps.gz) (Abgabe bis 4. Juni)
Übung 8 (ps.gz) (Abgabe 10. Juni)
Übung 9 (ps.gz) (Abgabe 17. Juni)
Übung 10 (ps.gz) (Abgabe 24. Juni)
Übung 11 (ps.gz) (Abgabe 1. Juli)

Literatur

Kurzbeschreibung und Inhaltsangabe

Inhaltsübersicht:

13. April bis 20. Mai:
Die imperative Beispielsprache IMP
Abstrakte Syntax von IMP (html)
Operationelle Einschrittsemantik von IMP (ps.gz)
Operationelle Ergebnissemantik von IMP (ps.gz)
Beziehung zwischen Einschritt-  und Ergebnissemantik
Denotationelle Semantik von IMP (ps.gz)
Beziehung zwischen operationeller und denotationeller Semantik
Axiomatische Semantik: Hoare-Kalkül (ps.gz)
Korrektheit des Hoare-Kalküls
Schwächste Vorbedingungen (ps.gz)
Relative Vollständigkeit des Hoare-Kalküls
Dazu: Ersetzung von wp-Prädikaten durch äquivalente ohne wp (ps.gz)

20. Mai bis 1. Juni:
Einführung in die Bereichstheorie
Posets und kleinste obere Schranken
Cpos und stetige Funktionen zwischen cpos
Produkte von cpos, Cpo der stetigen Funktionen, Liften von cpos
kleinste Fixpunkte, Fixpunktinduktion, Park-Kriterium, Bekic-Theorem

8. bis 29. Juni:
Die funktionale Beispielsprache FUN
Syntax und Typisierung (ps.gz)
Operationelle Semantik (ps.gz) mit Auswertungskontexten
Denotationelle Semantik (ps.gz)
Beziehung zwischen call-by-value und call-by-name
Beziehung zwischen operationeller und denotationeller Semantik
Verschiedene Arten von Äquivalenzen zwischen Termen
Nichtdarstellbarkeit des "Parallelen Oder"

1. bis 15. Juli:
Erweiterung um Produkttypen und Summentypen; Einertyp
Rekursive Typen und rekursive cpo-Definitionen (cpo-Gleichungen)
Methoden zur Lösung von cpo-Gleichungen (Überblick)
Informationssysteme (einfacher als die im Winskel-Buch)
Produkt, Summe und Funktionskonstruktion bei Informationssystemen
Anwendung in der denotationellen Semantik
Rekursion ohne syntaktische Hilfsmittel


Reinhold Heckmann / heckmann@absint.com