Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage...- die Semantik von neuen Programmkonstrukten zu spezifizieren.- die Korrektheit eines Programmes anhand der Semantik der Programmiersprache zu beweisen.- die verschiedenen Arten, die Semantik einer Programmiersprache zu spezifizieren, zu vergleichen und die geeignete Semantik für eine Problemstellung auszuwählen.- Beweise über die Semantik einer Programmiersprache zu führen, insbesondere geeignete Induktionsargumente anzuwenden.
Die Vorlesung führt in die verschiedenen Möglichkeiten ein die Semantik von Programmiersprachen zu beschreiben. Während die Syntax einer Programmiersprache festlegt, welche sprachlichen Konstrukte zur Verfügung stehen, legt die Semantik die Bedeutung dieser Konstrukte fest. Hierfür benützen wir mathematische Methoden um die Bedeutung von Programmkonstrukten präzise und konzise zu beschreiben. Die Semantik von Programmiersprachen ist die Grundlage um argumentieren zu können ob ein Programm das tut was man erwartet. Eine präzise Beschreibung der Semantik ist beispielsweise zwingend erforderlich um zu argumentieren, dass ein Compiler C-Programme korrekt in Maschinensprache übersetzt (siehe das CompCert Projekt, http://compcert.inria.fr/) oder um zu beweisen, dass ein Programm funktional korrekt und frei von bestimmten Fehlerklassen ist (siehe das seL4 Microkernel Projekt, https://sel4.systems/, welches zum Beispiel das Auftreten von buffer-overflows ausschließt.) Ein Beispiel für einen aktuellen Forschungsgegenstand sind Korrektheitskriterien für moderne nebenläufigen Prozessoren die Speicherlese- und Schreibzugriffe aus Effiziensgründen umordnen düfen (siehe https://en.wikipedia.org/wiki/Memory_ordering).
In der Vorlesung besprechen wir- die operationale, denotationale und axiomatische Semantik einer einfachen imperativen Programmiersprache.- die Zusammenhänge zwischen den verschiedenen Semantiktypen (operational, denotational und axiomatisch).- mathematische Beweistechnicken um über die Semantik eines Programms zu argumentieren, insbesondere verschiedene Techniken für Induktionsbeweise.- ausgewählte Themen wie Nichtdeterminismus und Nebenläufigkeit.- wie man die Korrektheit eines Compilers beweisen kann.- die operationale Semantik und das Typsystem einer einfachen funktionalen Programmiersprache, sowie die Korrektheit des Typsystems bezüglich der operationalen Semantik.
Die Vorlesung besteht aus Vorlesungen + 5 Übungen.
In den Übungen setzen sich die Studierenden aktiv mit dem Material aus der Vorlesung auseinander. Hierzu gibt es in jeder Übung ein Übungsblatt, welches von den Studierenden bearbeitet wird. In den Übungsaufgaben erlernen die Studierenden- die Semantik von neuen Programmkonstrukten zu spezifizieren.- die Korrektheit eines Programmes anhand der Semantik der Programmiersprache zu beweisen.- die verschiedenen Arten, die Semantik einer Programmiersprache zu spezifizieren, zu vergleichen und die geeignete Semantik für eine Problemstellung auszuwählen.- Beweise über die Semantik einer Programmiersprache zu führen, insbesondere geeignete Induktionsargumente anzuwenden.
ECTS Breakdown: ECTS 4.5 = 112 Std.
Vorlesungsteil: 8 Einheiten zu je 5 Stunden: 40 Std.
Ausarbeitung und Präsentation der Übungsblätter: 50 Std.
Prüfung inkl. Vorbereitungszeit: 22 Std.
Beginn: Der Kurs beginnt am 3.3.2020.
Termine der Vorlesungen/Übungen/Examen für SS2020:
3.3. intro/lecture-FO-part15.3. lecture-FO-part2/ex-FO online10.3. lecture112.3. lecture2/ex1 online17.3. exercise-FO19.3. repetition 24.3. lecture3/ex2 online26.3. TBA 31.3. lecture42.4. exercise17.4. Easter Break9.4. Easter Break14.4. Easter Break16.4. Easter Break21.4. lecture5/ex3 online23.4. TBA28.4. exercise2 30.4. lecture65.5. TBA 7.5. lecture7/ex4 online12.5. lecture814.5. exercise319.5. lecture9/ex5 online21.5. Public Holiday (Christi Himmelfahrt)26.5. exercise4 28.5. TBA2.6. University Holiday (Pfingstferien)4.6. exercise59.6. 11.6. Public Holiday (Fronleichnam)16.6. exam18.6.23.6. 25.6.30.6. if needed: exam repetition
------
Weiterführende Literatur:
"Introduction to lattices and order", B. A. Davey and H. A. Priestley ist eine gute Einführung in Verbandstheorie (lattice theory)
"Types and Programming Languages", Benjamin Pierce ist die Standardeinführung für Typen in Programmiersprachen
Am Ende des Semester gibt es eine schriftliche Prüfung (open-book) über 2 Stunden. Die Aufgaben der schriftlichen Prüfung orientieren sich an den Übungsaufgaben der Übungsblätter.
Keine.
Grundlegende Kenntnisse über first-order logic (FOL) wie in den Vorlesungen 185.278 und 185.291 eingeführt; insbesondere,das Verstehen des Unterschiedes zwischen Syntax und Semantik sowie die Handhabung des Beweisprinzips strukturelle Induktion um Eigenschaften von FOL Formeln beweisen zu können.
Grundlegende Kenntnisse über Hoare-Logik wie in der Vorlesung 185.291 eingeführt.
Sicheres Handhaben mengentheoretischer und logischer Notation; insbesondere, das präzise Formulieren und Beweisen mathematischer Aussagen wie in den Kursen 104.271, 185.278, 185.291 gelehrt und praktiziert.
