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.

2021S, 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 23.3.2021.

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

Jeden Dienstag, 13:00-15:00

Schedule

23.3. Q&A 1
30.3. Ostern
6.4.   Ostern
13.4. FO-exercise sheet/ repetition-sheet
20.4. Q&A 2
27.4. exercise 1
4.5.  Q&A 3
11.5. exercise 2
18.5. Q&A 4
25.5. Pfingsten
1.6.  exercise 3
8.6.  Q&A 5
15.6. exercise 4
22.6. exercise 5
29.6. exam


Vorlesungen werden vorab auf Video aufgenommen und online gestellt. Der Vorlesungstermin wird für Q&A sessions über die Vorlesungsinhalte benutzt sowie für die Besprechung der Übungsaufgaben. Der präzise Vorlesungsmodus wird zum 23.3.2021 besprochen. Die Vorlesungsfolien des vergangenen Semesters wurden bereits online gestellt (die Folien werden möglicherweise im aktuellen Semester angepasst).

------

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

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
12.02.2021 09:00 25.04.2021 22:00 26.05.2021 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