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

Termine der Vorlesungen/Übungen/Examen 

3.3. lecture FO part1

7.3. lecture FO part2/ex-FO online

10.3. lecture1

14.3. lecture2/hand-in ex-FO/ex1 online

17.3. exercise FO

4.4. repitition

7.4. lecture3/hand-in ex1/ex2 online

11.4. lecture4

14.4. exercise1

18.4. lecture5/hand-in ex2/ex3 online

21.4. lecture6

25.4. exercise2

28.4. TBA(probably no lecture)

2.5. lecture7/hand-in ex3/ex4 online

9.5. lecture8

12.5. exercise3

19.5. TBA(probably no lecture)

23.5. TBA(probably no lecture)

30.5. last lecture/hand-in ex4/ex5 online

2.6. TBA(probably no lecture)

6.6. exercise4/hand-in ex5

9.6. TBA(probably no lecture)

13.6. exercise5

16.6. TBA(probably no lecture)

20.6. exam1

23.6. no lecture

27.6. no lecture

30.6. exam2

 ------

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.

Die Teilnahme an diesem Kurs erfordert das Bestehen eines Eingangstests, der in der dritten Vorlesung stattfinden wird. Der Eingangstest hat first-order logic und einfache aber sauber ausgeführte Beweise zum Thema (siehe Zugangsvorraussetzungen). Der Eingangstest wird bewertet im Hinblick auf die Sauberkeit der mathematischen Formulierungen und Schlussfolgerungen. Der Eingangstest kann entweder bestanden oder nicht bestanden werden und trägt nicht zur Endnote bei.

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.

Diese Vorraussetzungen werden in dem Eingangstest abgefragt werden.