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.

2020S, VU, 3.0h, 4.5EC
Diese Lehrveranstaltung wird nach dem neuen Modus evaluiert. Mehr erfahren

LVA-Bewertung

Merkmale

  • Semesterwochenstunden: 3.0
  • ECTS: 4.5
  • Typ: VU Vorlesung mit Übung

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

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

3.3. intro/lecture-FO-part1
5.3. lecture-FO-part2/ex-FO online
10.3. lecture1
12.3. lecture2/ex1 online
17.3. exercise-FO
19.3. repetition
24.3. lecture3/ex2 online
26.3. TBA
31.3. lecture4
2.4. exercise1
7.4. Easter Break
9.4. Easter Break
14.4. Easter Break
16.4. Easter Break
21.4. lecture5/ex3 online
23.4. TBA
28.4. exercise2
30.4. lecture6
5.5.   TBA 
7.5. lecture7/ex4 online
12.5. lecture8
14.5. exercise3
19.5. lecture9/ex5 online
21.5. Public Holiday (Christi Himmelfahrt)
26.5. exercise4
28.5. TBA
2.6. University Holiday (Pfingstferien)
4.6. exercise5
9.6.
11.6. Public Holiday (Fronleichnam)
16.6. exam
18.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

Vortragende

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Di.13:00 - 15:0003.03.2020 - 10.03.2020Seminarraum FAV EG C (Seminarraum Gödel) Semantik von Programmiersprachen
Do.13:00 - 15:0005.03.2020 - 12.03.2020Seminarraum FAV EG C (Seminarraum Gödel) Semantik von Programmiersprachen
Semantik von Programmiersprachen - Einzeltermine
TagDatumZeitOrtBeschreibung
Di.03.03.202013:00 - 15:00Seminarraum FAV EG C (Seminarraum Gödel) Semantik von Programmiersprachen
Do.05.03.202013:00 - 15:00Seminarraum FAV EG C (Seminarraum Gödel) Semantik von Programmiersprachen
Di.10.03.202013:00 - 15:00Seminarraum FAV EG C (Seminarraum Gödel) Semantik von Programmiersprachen
Do.12.03.202013:00 - 15:00Seminarraum FAV EG C (Seminarraum Gödel) Semantik von Programmiersprachen

Leistungsnachweis

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.

LVA-Anmeldung

Von Bis Abmeldung bis
14.02.2020 09:00 26.04.2020 22:00 27.05.2020 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