Master-Pflichtmodul MPM1: Formale Grundlagen der Informatik III (FGI-3)


Veranstaltungs-Nr.: VL 64-301 (WiSe 2009/2010)
Titel: Vorlesung FGI 3 - Semantik von Programmen
Veranstalter: Matthias Jantzen
Zeit / Ort: 2 st. Beginn 20.10. 2009, Di. 14:15-15:45 B-201
-
Kommentare/ Inhalte:

Informatiksysteme und ihre Teilsysteme werden syntaktisch kodiert, um ein bestimmtes Erscheinungsbild, speziell ein bestimmtes Verhalten zu erzielen, das eine vorgegebene Spezifikation erfüllen muss. Leitmotiv dieses Moduls ist daher die Trias System-Verhalten-Spezifikation oder mit etwas versetzter Perspektive Syntax Semantik-Logik. Syntax leitet den konsistenten Entwurf von Programmierformalismen (d.h. auf textueller Basis Programmiersprachen oder mit graphischen Mitteln Modellierungswerkzeuge) in Hinblick auf erwartete Reaktionen des Systems. Die formale Beschreibung des Systemverhaltens durch verschiedene Methoden der Semantik ist auch erforderlich, um Portabilität (d.h. Ausführung auf verschiedenen Plattformen) oder Mobilität (d.h. Ausführung in verschiedenen Umgebungen) zu erzielen. Logische Methoden sind als universaler Ansatz für alle Teile der Trias von Bedeutung. (System-) Spezifikationen werden in speziellen Logiken formuliert, um Verifikationswerkzeuge mit praktikabler Komplexität zu realisieren. Logische Methoden werden jedoch auch in der Semantik (z.B. axiomatische Semantik) oder als Programmiersprache (z.B. Prolog) eingesetzt.


Inhalte des Vorlesungsteils "Semantik von Programmen":

  • Denotationale Semantik, Domainen und stetige Funktionen, Fixpunktsatz,
  • Formale Spezifikation, Programmverifikation, axiomatische Semantik, Hoare-Tripel, Beweis-Kalküle,
  • Illustration der denotationalen Semantik bei zusammengesetzten Datenstrukturen, Fehlerbehandlung, Ein/Ausgabe,
  • Operationale Semantik und Nichtdeterminismus, Semantik von nebenläufigen Programmen
  • Reduktionssysteme, Gleichungslogik und universelle Algebra, Identitäten und Datentypspezifikationen, bedingte Ersetzungssysteme.
Lernziel:Das Modul behandelt über den Bachelorstoff hinausgehende Konzeptionen der Logik und Semantik, und legt somit die Grundlage für eine vertieftes Verständnis formaler Ansätze zur Spezifikation von Informatiksystemen, wie sie für ein wissenschaftliches Vorgehen in allen Vertiefungsgebieten des Masterstudiums benötigt werden. Die beiden Themenbereiche Logik und Semantik von Programmen werden durch zwei aufeinander abgestimmte Vorlesungen (jeweils 2 SWS) behandelt. Inhaltliche Schwerpunkte dieser Vorlesung des Moduls sind klassische Themen der formalen Semantik. Darüber hinaus gehört zu dem Modul ein integriertes Seminar, das ausgewählte theoretische Konzeptionen vertieft. Durch diese exemplarischen Vertiefungen an Hand von Originalarbeiten werden die Masterstudierenden darin trainiert, klassische und aktuelle Arbeiten der theoretischen Informatik und der Logik zu lesen, und mit Fragestellungen der Informatik der Systeme in Beziehung zu setzen.
Stell. im Studienplan: Hauptstudium, Master (3 LP); Modul MPM1
Voraussetzungen:Verbindlich: keine
Empfohlen: Grundkenntnisse der Formalen Grundlagen und der Programmierung entsprechend dem Bachelor-Studiengang Informatik
Vorgehen:Vorlesung. Die Zulassung zur Modulprüfung setzt die regelmäßige und erfolgreiche (Seminararbeit und Referat) Teilnahme an dem integrierten Seminar voraus. Die Modulprüfung findet als Modulabschlussprüfung in Form einer mündlichen Prüfung (über die Gesamtinhalte der Vorlesungsanteile und des Seminaranteils) in der Unterrichtssprache statt.
Verwendbarkeit:Teil des Master Pflichtmoduls MPM1,
gemeisam mit 18.300 im Diplomstudiengang Informatik als Grundlagenvorlesung LOS (Logik und Semantik) anrechenbar.
Literatur:
  • J.C. Reynolds: Theories of Programming Languages (Cambridge University Press, 1998) [T REY],
  • J.C. Mitchell: Foundations for Programming Languages (The MIT Press, 1996) [T MIT],
  • D. Gries: The Science of Programming (Springer, 1981) [T GRI],
  • A.R. Hoare; Unifying Theories of Programming (Prentice Hall, 1998) [T HOA],
  • B. Meyer: Introduction to the Theory of Programming Languages (Prentice Hall, 1990) [T MEY]
  • F. Baader, T. Nipkow: Term Rewriting and All That, Cambridge Univ. Press, 1998 [T BAA]
  • H. Ehrig, B. Mahr: Fundamentals of Algebraic Specification 1, Springer, Berlin, 1985 [T EHR]
Periodizität:jährlich zum WS
Sprache:Deutsch
Eignung:Geeignet für Lehramtsstudierende, Nebenfachstudierende, Bioinformatikstudierende, Wirtschaftsinformatikstudierende.
Stichwörter:Domains, Fixpunktsatz, Syntax, Reduktionssystem, universelle Algebra, algebraische Datentypspezifikation, bedingte Ersetzungssysteme, denotationale, axiomatische und operationale Semantik