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 7.3.2022.
Termine der Vorlesungen/Übungen/Examen für SS2023:
Jeden Dienstag, Donnerstag, 10:00-12:00
Schedule
2.3. no lecture
7.3. Q&A 1 (first-order-logic/intro/lecture1)
9.3. Q&A 2 (lecture2)
14.3. FO-exercise sheet/ repetition-sheet
16.3. Q&A 3 (lecture3)
21.3. Q&A 4 (lecture4)
23.3. exercise 1
28.3. Q&A 5 (lecture5)
30.3. exercise 2
4.4. Osterferien
6.4. Osterferien
11.4. Osterferien
13.4. Osterferien
18.4. no lecture
20.4. Q&A 6 (lecture6)
25.4. exercise 3
27.4. Q&A 7 (lecture7)
2.5. Q&A 8 (lecture8)
4.5. exercise 4
16.5. no lecture
18.5. Christi Himmelfahrt
23.5. Q&A 9 (lecture9)
25.5. tba
30.5. TU Pfingstferien
1.6. exercise 5
6.6.
8.6. Fronleichnam
13.6. exam
15.6.
20.6.
22.6.
27.6.
29.6.
Vorlesungsmodus:
Geplant ist ein Inverted-Classroom modus mit vorab aufgezeichneten Videos und Q&A Sitzungen im Vorlesungssaal. (Wenn jedoch die Mehrheit der StudentInnen live-Vorlesungen bevorzugt, können In-Classroom Vorlesungen abgehalten werden. Dies wird zum ersten Vorlesungstermin am 7.3. besprochen. Für den 7.3. werden die StudentInnen gebeten, sich die für diesen Termin geplanten Videos anzusehen.)
Vorlesungen und Folien werden vorab auf Video aufgenommen und online gestellt. Die StudentInnen werden gebeten sich die Videos vorab selbständig anzusehen. Fragen zu den Vorlesungen können jeweils in den Q&A sessions besprochen werden. Die Videos, die in den Q&A sessions besprochen werden, sind in den Klammern der jeweiligen Q&A session angegeben. Um die Unterrichtsmaterialien einsehen zu können, ist es notwendig sich für die Vorlesung anzumelden. Es gibt 5 Übungsblätter + ein extra Übungsblatt zu first-order Logik, welche vorab zu lösen sind, und die dann in den Übungssessions vorzurechnen sind (mit Ankreuzen der vorbereiteten Übungsaufgaben). Die Vorlesung beginnt mit der Q&A session am 7.3.2022, in der auch der Vorlesungsmodus nochmal besprochen wird. (Beachten Sie, dass die Vorlesungsaufzeichnungen vom SS2021 stammen. Daher sind die Datumsangaben in den Vorlesungsaufzeichnungen nicht korrekt.)
------
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
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.
