|
Theorie der Programmierung (ThProg)7.5 ECTS (englische Bezeichnung: Theory of Programming)
(Prüfungsordnungsmodul: Theorie der Programmierung)
Modulverantwortliche/r: Lutz Schröder Lehrende:
Lutz Schröder, Daniel Gorin, Tadeusz Litak
Start semester: |
SS 2014 | Duration: |
1 semester | Cycle: |
jährlich (SS) |
Präsenzzeit: |
90 Std. | Eigenstudium: |
135 Std. | Language: |
Deutsch |
Lectures:
Inhalt:
- Termersetzungssysteme, Normalisierung, Konfluenz
Getypter und ungetypter Lambda-Kalkül
Semantik von Programmiersprachen, Anfänge der Bereichstheorie
Datentypen, Kodatentypen, Induktion und Koinduktion, Rekursion
und Korekursion
Programmverifikation, Floyd-Hoare-Kalkül
Reguläre Sprachen und endliche Automaten
Beschriftete Transitionssysteme, Bisimulation und Temporallogik
Lernziele und Kompetenzen:
- Fachkompetenz
- Wissen
- Die Studierenden geben elementare Definitionen und Fakten zu den behandelten Formalismen wieder.
- Verstehen
- Die Studierenden
erläutern Grundbegriffe der Syntax und Semantik von Formalismen und setzen diese zueinander in Bezug
beschreiben und erklären grundlegende Algorithmen zu logischem Schließen und Normalisierung
beschreiben wichtige Konstruktionen von Modellen, Automaten und Sprachen
- Anwenden
- Die Studierenden
verfassen formale Spezifikationen sequentieller und nebenläufiger Programme
verifizieren einfache Programme gegenüber ihrer Spezifikation durch
Anwendung der relevanten Kalküle
setzen formale Sprachen mit entsprechenden Automaten in
Beziehung
führen einfache Beweise über Programme mittels Induktion und Koinduktion
- Analysieren
- Die Studierenden
wählen für gegebene Verifikationsprobleme geeignete Formalismen aus
erstellen einfache Meta-Analysen formaler Systeme, etwa Konfluenzprüfung von Termersetzungssystemen
- Lern- bzw. Methodenkompetenz
- Die Studierenden beherrschen das grundsätzliche Konzept des Beweises als hauptsächliche Methode des Erkenntnisgewinns in der theoretischen Informatik. Sie überblicken abstrakte Begriffsarchitekturen.
- Sozialkompetenz
- Die Studierenden lösen abstrakte Probleme in kollaborativer Gruppenarbeit.
Literatur:
- Glynn Winskel, Formal Semantics of Programming Languages, MIT Press, 1993
Michael Huth, Mark Ryan, Logic in Computer Science, Cambridge University Press, 2. Auflage 2004
Henk Barendregt, The lambda-Calculus: Its Syntax and Semantics, North Holland, 1984
John E. Hopcroft, Jeffrey D. Ullman and Rajeev Motwani, Introduction to Automata Theory, Languages, and Computation, 3rd ed., Prentice Hall, 2006
Franz Baader, Tobias Nipkow, Term Rewriting and All That, Cambridge University Press, 1999
Weitere Informationen:
Keywords: Lambda-Kalkül Verifikation Termersetzung Temporallogik Formale Sprachen Automaten
Verwendbarkeit des Moduls / Einpassung in den Musterstudienplan:
- Mathematik (Bachelor of Science)
(Po-Vers. 2009 | Nebenfach Informatik | Module im 2. und 3. Studienjahr | Wahlbereich 2 | Theorie der Programmierung)
Dieses Modul ist daneben auch in den Studienfächern "Informatik (Bachelor of Science)" verwendbar. Details
Studien-/Prüfungsleistungen:
Theorie des Programmierens (Klausur) (Prüfungsnummer: 31211)
- Prüfungsleistung, Klausur, Dauer (in Minuten): 90, benotet
- Anteil an der Berechnung der Modulnote: 100.0 %
- weitere Erläuterungen:
Die Rahmen der Übungen gestellten Übungsaufgaben können abgegeben werden und werden in diesem Fall bewertet. Auf Basis des Ergebnisses dieser Bewertungen können bis zu 15% Bonuspunkte erworben werden, die zu dem Ergebnis einer bestandenen Klausur hinzugerechnet werden.
- Erstablegung: SS 2014, 1. Wdh.: WS 2014/2015
- Termin: 02.10.2014, 13:00 Uhr, Ort: s. Aushang
Termin: 09.02.2015, 09:45 Uhr, Ort: H 8 TechF
Termin: 09.10.2015, 16:30 Uhr, Ort: H 11
Termin: 15.02.2016, 11:00 Uhr, Ort: H 8 TechF
|
|
|