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.

2019S, VU, 3.0h, 4.5EC

Merkmale

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

Ziele der Lehrveranstaltung

Vermittlung grundlegender Formalismen und Definitionsmethoden zur semantischen Beschreibung und Charakterisierung von Programmiersprachen und programmiersprachlichen Konstrukten. Erarbeitung methodischer Kriterien fuer die Analyse und den Korrektheitsnachweis eines Programmes in Bezug auf die Semantik der jeweiligen Programmiersprache.

Inhalt der Lehrveranstaltung

Grundlegende semantische Beschreibungsmethoden und Definitionsformalismen: Operationale, denotationale und axiomatische Semantik imperativer Programmierkonstrukte; Bezüge zur Programmverifikation; Einführung in den Lambda-Calculus; induktive und rekursive Definitionen; Fixpunkt-Operatoren und -Konstruktion; Vertiefung ausgewählter Themen wie Nichtdeterminismus und Nebenläufigkeit.

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

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

4.3. intro/ lecture FO part1
6.3. lecture FO part2 /ex-FO online
11.3. lecture1
13.3. lecture2/hand-in ex-FO/ex1 online
18.3. exercise FO
20.3. repetition
25.3. lecture3/hand-in ex1/ex2 online
27.3. lecture4
1.4. exercise1
3.4. lecture5/hand-in ex2/ex3 online
8.4. no lecture
10.4. exercise2
15.4. Easter holidays
17.4. Easter holidays
22.4. Easter holidays
24.4. Easter holidays
29.4. TBA
1.5. public holiday
6.5 lecture6
8.5. lecture7/hand-in ex3/ex4 online
13.5. lecture8
15.5. exercise3
20.5. lecture9/hand-in ex4/ex5 online
22.5. TBA
27.5. exercise4/hand-in ex5
29.5. TBA
3.6. exercise5
5.6. TBA
10.6. Holiday
12.6. exam
17.6. no lecture
19.6. no lecture
24.6. no lecture
26.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
Mo.13:00 - 15:0004.03.2019 - 24.06.2019Seminarraum FAV 05 (Seminarraum 186) Semantik von Programmiersprachen
Mi.11:00 - 13:0006.03.2019 - 26.06.2019Seminarraum FAV 05 (Seminarraum 186) Semantik von Programmiersprachen
Semantik von Programmiersprachen - Einzeltermine
TagDatumZeitOrtBeschreibung
Mo.04.03.201913:00 - 15:00Seminarraum FAV 05 (Seminarraum 186) Semantik von Programmiersprachen
Mi.06.03.201911:00 - 13:00Seminarraum FAV 05 (Seminarraum 186) Semantik von Programmiersprachen
Mo.11.03.201913:00 - 15:00Seminarraum FAV 05 (Seminarraum 186) Semantik von Programmiersprachen
Mi.13.03.201911:00 - 13:00Seminarraum FAV 05 (Seminarraum 186) Semantik von Programmiersprachen
Mo.18.03.201913:00 - 15:00Seminarraum FAV 05 (Seminarraum 186) Semantik von Programmiersprachen
Mi.20.03.201911:00 - 13:00Seminarraum FAV 05 (Seminarraum 186) Semantik von Programmiersprachen
Mo.25.03.201913:00 - 15:00Seminarraum FAV 05 (Seminarraum 186) Semantik von Programmiersprachen
Mi.27.03.201911:00 - 13:00Seminarraum FAV 05 (Seminarraum 186) Semantik von Programmiersprachen
Mo.01.04.201913:00 - 15:00Seminarraum FAV 05 (Seminarraum 186) Semantik von Programmiersprachen
Mi.03.04.201911:00 - 13:00Seminarraum FAV 05 (Seminarraum 186) Semantik von Programmiersprachen
Mo.08.04.201913:00 - 15:00Seminarraum FAV 05 (Seminarraum 186) Semantik von Programmiersprachen
Mi.10.04.201911:00 - 13:00Seminarraum FAV 05 (Seminarraum 186) Semantik von Programmiersprachen
Mo.29.04.201913:00 - 15:00Seminarraum FAV 05 (Seminarraum 186) Semantik von Programmiersprachen
Mo.06.05.201913:00 - 15:00Seminarraum FAV 05 (Seminarraum 186) Semantik von Programmiersprachen
Mi.08.05.201911:00 - 13:00Seminarraum FAV 05 (Seminarraum 186) Semantik von Programmiersprachen
Mo.13.05.201913:00 - 15:00Seminarraum FAV 05 (Seminarraum 186) Semantik von Programmiersprachen
Mi.15.05.201911:00 - 13:00Seminarraum FAV 05 (Seminarraum 186) Semantik von Programmiersprachen
Mo.20.05.201913:00 - 15:00Seminarraum FAV 05 (Seminarraum 186) Semantik von Programmiersprachen
Mi.22.05.201911:00 - 13:00Seminarraum FAV 05 (Seminarraum 186) Semantik von Programmiersprachen
Mo.27.05.201913:00 - 15:00Seminarraum FAV 05 (Seminarraum 186) Semantik von Programmiersprachen

Leistungsnachweis

Lehrveranstaltungsaufbau:

In den ersten beiden Vorlesungen wird eine Wiederholung von first-order logic stattfinden, die von denjenigen Studenten ausgelassen werden kann, die das Material bereits beherrschen. Dieses Jahr gibt es keinen Eingangstest. Allerdings werden im ersten Aufgabenblatt grundlegende Kenntnisse zu first-order logic (FOL) erwartet, sowie die sichere Handhabung mengentheoretischer und logischer Notation.

Der Hauptteil der Lehrveranstaltung besteht aus 8 Vorlesungseinheiten und 5 Übungsteilen.

Nach je 2 Vorlesungseinheiten muss ein Übungsblatt ausgearbeitet werden.

Die Ausarbeitung des ersten Übungsblattes zu first-order logic sowie der weiteren 5 Übungsblätter muss zu mindestens 40% richtig sein, um zur Prüfung zugelassen zu werden.

LVA-Anmeldung

Von Bis Abmeldung bis
15.02.2019 09:00 28.04.2019 22:00 29.05.2019 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