184.749 Semantik von Programmiersprachen
Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.
Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.

2022S, VU, 3.0h, 4.5EC

Merkmale

  • Semesterwochenstunden: 3.0
  • ECTS: 4.5
  • Typ: VU Vorlesung mit Übung
  • Format der Abhaltung: Distance Learning

Lernergebnisse

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.

Inhalt der Lehrveranstaltung

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.

Methoden

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.

Prüfungsmodus

Schriftlich

Weitere Informationen

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 8.3.2022.

Termine der Vorlesungen/Übungen/Examen für SS2022:

Jeden Dienstag, 12:00-14:00

Schedule

8.3. Q&A 1 (first-order-logic/intro/lecture1)
15.3. FO-exercise sheet/ repetition-sheet
22.3. Q&A 2 (lecture2/lecture3)
29.3. exercise 1
5.4. Q&A 3 (lecture4/lecture5)
12.4. Easter Holidays
19.4. Easter Holidays
26.4. exercise 2
3.5. Q&A 4 (lecture6/lecture7)
10.5. exercise 3
17.5. Q&A 5 (lecture8/lecture9)
24.5. exercise 4
31.5. tba
7.6. Pentecost Holidays
14.6. exercise 5
21.6. tba
28.6. exam


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 8.3.2022, in der auch der Vorlesungsmodus nochmal besprochen wird. Es ist geplant die Q&A sessions + Übungssessions + Exam in Präsenz abzuhalten, falls aufgrund der Pandemie notwendig wird auf online Unterricht umgestellt. (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

Vortragende Personen

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Di.12:00 - 14:0008.03.2022Seminarraum FAV EG B (Seminarraum von Neumann) Semantik von Programmiersprachen
Di.12:00 - 14:0022.03.2022 - 28.06.2022Seminarraum FAV EG C (Seminarraum Gödel) Semantik von Programmiersprachen
Semantik von Programmiersprachen - Einzeltermine
TagDatumZeitOrtBeschreibung
Di.08.03.202212:00 - 14:00Seminarraum FAV EG B (Seminarraum von Neumann) Semantik von Programmiersprachen
Di.22.03.202212:00 - 14:00Seminarraum FAV EG C (Seminarraum Gödel) Semantik von Programmiersprachen
Di.29.03.202212:00 - 14:00Seminarraum FAV EG C (Seminarraum Gödel) Semantik von Programmiersprachen
Di.05.04.202212:00 - 14:00Seminarraum FAV EG C (Seminarraum Gödel) Semantik von Programmiersprachen
Di.26.04.202212:00 - 14:00Seminarraum FAV EG C (Seminarraum Gödel) Semantik von Programmiersprachen
Di.03.05.202212:00 - 14:00Seminarraum FAV EG C (Seminarraum Gödel) Semantik von Programmiersprachen
Di.10.05.202212:00 - 14:00Seminarraum FAV EG C (Seminarraum Gödel) Semantik von Programmiersprachen
Di.17.05.202212:00 - 14:00Seminarraum FAV EG C (Seminarraum Gödel) Semantik von Programmiersprachen
Di.24.05.202212:00 - 14:00Seminarraum FAV EG C (Seminarraum Gödel) Semantik von Programmiersprachen
Di.31.05.202212:00 - 14:00Seminarraum FAV EG C (Seminarraum Gödel) Semantik von Programmiersprachen
Di.14.06.202212:00 - 14:00Seminarraum FAV EG C (Seminarraum Gödel) Semantik von Programmiersprachen
Di.21.06.202212:00 - 14:00Seminarraum FAV EG C (Seminarraum Gödel) Semantik von Programmiersprachen
Di.28.06.202212:00 - 14:00Seminarraum FAV EG C (Seminarraum Gödel) Semantik von Programmiersprachen

Leistungsnachweis

Am Ende des Semester gibt es eine mündliche Prüfung (mit whiteboard) über Zoom. Die Aufgaben der mündlichen Prüfung orientieren sich an den Übungsaufgaben der Übungsblätter.

LVA-Anmeldung

Von Bis Abmeldung bis
11.02.2022 09:00 24.04.2022 22:00 25.05.2022 22:00

Anmeldemodalitäten

Keine.

Curricula

Literatur

Es wird kein Skriptum zur Lehrveranstaltung angeboten.

Vorkenntnisse

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.

 

Vorausgehende Lehrveranstaltungen

Sprache

Englisch