|
Theorie der Programmierung (ThProg)7.5 ECTS (englische Bezeichnung: Theory of Programming)
Modulverantwortliche/r: Lutz Schröder Lehrende:
Lutz Schröder, Christoph Rauch
Startsemester: |
SS 2017 | Dauer: |
1 Semester | Turnus: |
jährlich (SS) |
Präsenzzeit: |
90 Std. | Eigenstudium: |
135 Std. | Sprache: |
Deutsch |
Lehrveranstaltungen:
-
-
Theorie der Programmierung
(Vorlesung, 4 SWS, Lutz Schröder, Mo, 14:15 - 15:45, C1 - Chemikum; Do, 16:15 - 17:45, H9)
-
Übungen zu Theorie der Programmierung
(Übung, 2 SWS, Christoph Rauch)
-
Intensivübung zu Theorie der Programmierung (optional)
(Übung, 2 SWS, Christoph Rauch, Fr, 14:15 - 15:45, 0.68)
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:
Schlüsselwörter: Lambda-Kalkül Verifikation Termersetzung Temporallogik Formale Sprachen Automaten
Verwendbarkeit des Moduls / Einpassung in den Musterstudienplan: Das Modul ist im Kontext der folgenden Studienfächer/Vertiefungsrichtungen verwendbar:
- Informatik (Bachelor of Science): 4. Semester
(Po-Vers. 2009w | TechFak | Informatik (Bachelor of Science) | weitere Pflichtmodule | Theorie der Programmierung)
Studien-/Prüfungsleistungen:
Theorie des Programmierens (Klausur) (Prüfungsnummer: 31211)
- Prüfungsleistung, Klausur, Dauer (in Minuten): 90, benotet, 7.5 ECTS
- Anteil an der Berechnung der Modulnote: 100.0 %
- weitere Erläuterungen:
Die im 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 2017, 1. Wdh.: WS 2017/2018 (nur für Wiederholer)
- Termin: 13.10.2017, 16:00 Uhr, Ort: Mensa-Süd
Termin: 19.02.2018, 08:00 Uhr, Ort: H 9 TechF
Termin: 12.10.2018, 13:30 Uhr, Ort: s. Aushang
Termin: 18.02.2019, 08:00 Uhr, Ort: K 1 TechF
|
![](/img/anew/void.gif) |
![](/img/anew/void.gif) |
|
UnivIS ist ein Produkt der Config eG, Buckenhof |
|
|