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 5.3.2018.
Termine der Vorlesungen/Übungen/Examen
5.3. intro/ lecture FO part1
7.3. lecture FO part2 /ex-FO online
12.3. lecture1
14.3. lecture2/hand-in ex-FO/ex1 online
19.3. exercise FO
21.3. repitition
26.3. Easter holidays
28.3. Easter holidays
2.4. Easter holidays
4.4. Easter holidays
9.4. lecture3/hand-in ex1/ex2 online
11.4. lecture4
16.4. exercise1
18.4. lecture5/hand-in ex2/ex3 online
23.4. lecture6
25.4. exercise2
30.4. lecture7/hand-in ex3/ex4 online
2.5. lecture8
7.5. exercise3
9.5. no lecture
14.5. no lecture
16.5. lecture9/hand-in ex4/ex5 online
21.5. Pfingstmontag / public holiday
23.5. exercise4/hand-in ex5
28.5. TBA
30.5. exercise5
4.6. TBA
6.6. exam1
11.6. no lecture
13.6. no lecture
18.6. no lecture
20.6. no lecture
25.6. exam2
27.6. no lecture
------
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.
