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: 5 Einheiten zu je 8 Stunden: 40 Std.
Ausarbeitung und Präsentation der Übungsblätter: 50 Std.
Prüfung inkl. Vorbereitungszeit: 22 Std.
Beginn: Der Kurs beginnt am 8.6.2017.
Termine der Vorlesungen/Übungen/Examen
8.6. lecture FO-part1/lecture FO-part2/exercise-FO online
9.6. lecture1/lecture2
12.6. exercise-FO/exercise-sample/exercise1 online
13.6. lecture3/lecture4
14.6. exercise1
16.6. lecture5/lecture6
19.6. exercise2
20.6. lecture7/lecture8
21.6. exercise3
22.6. TBA (probably no lecture)
23.6. exercise4
26.6. TBA (probably no lecture)
27.6. exercise5
30.6. Written Exam
Es wird einen Wiederholungstermin in der ersten Woche des WS17/18 geben, der genaue Termin wird noch angekündigt.
------
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:
Die Lehrveranstaltung findet dieses Jahr geblockt im Juni statt.
(SS 2018 wird die Vorlesung wieder regulär über das Semester verteilt stattfinden.)
In der ersten Vorlesung gibt es eine Wiederholung von first-order logic, die von denjenigen Studenten ausgelassen werden kann, die das Material bereits beherrschen. Es gibt es keinen Eingangstest. Allerdings werden im ersten Aufgabenblatt grundlegende Kenntnisse zu first-order logic (FOL) erwartet, sowie die sichere Handhabung mengentheoretischer und logischer Notationen.
Der Hauptteil der Lehrveranstaltung besteht aus 4 Vorlesungseinheiten und 6 Übungseinheiten.
In den Übungseinheiten wird jeweils ein Aufgabenblatt besprochen. Das Aufgabenblatt wird bereits vorab online gestellt, so dass die Studenten sich mit den Aufgaben beschäftigen und auf die Übungsstunde vorbereiten können. Eine Abgabe der Übungsblätter ist nicht erforderlich. Die schriftliche Prüfung orientiert sich stark an den Übungsaufgaben. Daher ist eine intensive Beschäftigung mit den Übungsaufgaben Vorraussetzung für ein erfolgreiches Bestehen der Prüfung ist.
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.
