Zur Hauptnavigation Zum Inhaltsbereich Zur Suche Zum Seitenfuß

Master-Modul MPM1: Semantik
Formale Grundlagen der Informatik III (FGI-3)
(Wintersemester 2014/15)

Veranstalter: Dr. Manfred Kufleitner

Termin: Fr 14:15-15:45 in B-201

Aktuelles und Inhalte der Vorlesung

  • 30.01.15: Rekursive Gleichungen REC, einfache Beispiele, call-by-value, call-by-name, REC ist Turing-mächtig, Codierung von Booleschen Ausdrücken durch Terme, operationale Semantik von REC, denotationale Semantik von REC, die beiden Semantiken stimmen überein, kurze Wiederholung des Vorlesungsstoffs an der Tafel. Folien

  • 23.01.15: Übungsaufgaben zu Termination, Satz von Ramsey, Terminationsbeweise mit Hilfe des Lemmas von Dickson, Axiomatische Semantik von Arrays, Datentypen und statische Typbindung. Folien

  • 16.01.15: Paralleloperator: Syntax, Semantik, Beispiele; Nichtdeterminismus: Definition, Syntax, Beispiele; starke und schwache Fairness; Guarded Commands: Syntax, Semantik, Beispiele; Kommunizierende Prozesse; Transitionssysteme mit Kantenbeschriftungen; operationale Semantik für kommunizierende Prozesse; starke Bisimulationen. Folien

  • 09.01.15: Übungsaufgaben zur axiomatischen Semantik. Folien

  • 19.12.14: Die schächste Vorbedingung lässt sich effektiv durch eine Zusicherung beschreiben, partielle Korrektheitsaussagen mit schächsten Vorbedingungen lassen sich herleiten, Vollständigkeit des Hoare-Kalküls, der Gödelsche Unvollständigkeitssatz. Folien

  • 12.12.14: Widerholung partielle Korrektheitsaussagen und Hoare-Kalkül, Beispiel Plateau-Problem, Beispiel Potenzieren, Unentscheidbarkeit und Nicht-Aufzählbarkeit von gültigen Korrektheitsaussagen, schwächste Vorbedingungen als Mengen von Speicherbelegungen, schwächste Vorbedingungen als Zusicherungen, das Gödelsche beta-Prädikat, Aufgaben. Folien

  • 28.11.14: Axiomatische Semantik, Vorbedingung, Nachbedingung, partielle Korrektheitsaussagen, Beispiel Fakultätsprogramm, totale Korrektheitsaussagen, erweiterte arithmetische Ausdrücke, Zusicherungen, freie Variablen, Interpretation der freien Variablen, Semantik von Zusicherungen, partielle Funktionen mittels Bottom-Element, Gültigkeit von partiellen Korrektheitsaussagen, der Hoare-Kalkül, Korrektheit des Hoare-Kalküls. Folien

  • 21.11.14: Bunt gemischte Übungsaufgaben. Folien

  • 14.11.14: Denotationale Semantik; Definitionen für skip, Zuweisungen, Hintereinanderausführung, if-Anweisung; cond-Funktion; Gamma-b-c; Stetigkeit von Gamma-b-c; Definition der denotationalen Semantik der while-Schleife; denotationale Semantik und operationale Semantik stimmen überein; Beispiel Fakultätsfunktion; Aufgaben: Programm für Bottom, Definitionsbereich von Gamma-b-c hoch i von Bottom, b und c, so dass alle Funktionen Fixpunkt von Gamma-b-c sind. Folien

  • 07.11.14: Transitionssysteme, Determinismus, durch Transitionssysteme definierte Funktionen, Einzelschrittsemantik, Determiniertheit des zugehörigen Transitionssystems, Assioziativität der Hintereinanderausführung, Bigstep-Semantik, Äquivalenz von Einzelschrittsemantik und Bigstep-Semantik, while-Schleife in einer if-Anweisung. Folien

  • 31.10.14: Regelmenge, Beweis und Beweisbarkeit, Teilbeweis, Wohlordnung auf Beweisen, Regelinduktion, gerichtete Menge, CPOs, stetige Abbildungen,Fixpunkt, Fixpunktsatz von Kleene, flache Bereiche, partielle Abbildungen, stetige Abbildungen als CPO. Folien

  • 24.10.14: Relationen und Abbildungen, Äquivalenzrelationen, partielle Ordnungen, total/linear, strenge/strikte Ordnung, minimale Elemente, wohlfundiert, Wohlordnung, obere Schranke, Supremum, vollständiger Verband, Kette, Antikette, Wohl-Quasi-Ordnung (WQO), Lemma von Dickson, noethersche Induktion, Signatur, Terme, Teiltermrelation, strukturelle Induktion. Folien

  • 22.10.14: Mit folgendem Aufgabenblatt können Sie das Rechnen mit Funktionen und Relationen etwas üben. Die Aufgaben sind freiwillig und werden nicht besprochen.

  • 17.10.14: Beispiele zur Abgrenzung von Syntax und Semantik, Semantik-Funktionen, Programmiersprache IMP, Arithmetische Ausdrücke, Boolesche Ausdrücke, Programme, Operationale/Denotationale/Axiomatische Semantik mittels Beispielen. Folien

Überblick

Eine Hauptaufgabe der Semantik von Programmsprachen besteht also darin, implementationsunabhängige, in sich konsistente Definitionen von Syntax und Semantik zu finden. Beispielsweise enthielten frühe Definitionen von Programmsprachen keine Konzepte für Ein- und Ausgabe, da diese zu abhängig vom jeweils benutzten Rechner waren. Gesichtspunkte der Migration, Kooperation und Erlernbarkeit erfordern auch hier einheitliche Konzepte.

Die Vorlesung umfasst folgende Bereiche:

  • Semantik imperativer Programmiersprachen. Fundamentale Ansätze sind die operationale und die denotationale Semantik.
  • Axiomatische Semantik, die ein Kalkül zur syntaxorientierten Form der Programmverifikation bereitstellt.
  • Die Theorie abstrakter Datentypen, bei der das Konzept der Syntax insofern erweitert wird, als dass axiomatisch die Gültigkeit einer Menge von Gleichungen gefordert wird.
  • Semantik funktionaler Programmiersprachen.

Unterlagen zu früheren Vorlesungen

Das folgende Skript von Michael Köhler-Bußmeier stammt vom WiSe 2012/13. Es unterscheidet sich von dieser Vorlesung in der Reihenfolge der behandelten Themen sowie in der verwendeten Syntax. Die Inhalte sind weitgehend identisch. Die folgenden Foliensätze sind aus dem WiSe 2012/13.

Literatur

  • T. Nipkow, G. Klein. Concrete Semantics. [online]
  • J. C. Reynolds. Theories of Programming Languages. Cambridge University Press, 1998.
  • G. Winskel. The Formal Semantics of Programming Languages. MIT Press, 1993.
Impressum
Letzte Änderung: 10:57 23.06.2015   Seitenanfang