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