Theorie der Programmierung (ThProg)7.5 ECTS
(englische Bezeichnung: Theory of Programming)

Lehrveranstaltungen:

• • Theorie der Programmierung
    (Vorlesung, 4 SWS, Lutz Schröder, Mo, Do, 14:15 - 15:45, H4)
  • Übungen zu Theorie der Programmierung
    (Übung, 2 SWS, Daniel Hausmann)
  • Intensivübung zu Theorie der Programmierung (optional)
    (Übung, 2 SWS, Daniel Hausmann, Fr, 10:15 - 11:45, H14)

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

  • führen einfache Meta-Beweise über Formalismen mittels Induktion und Koinduktion

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:

Verwendbarkeit des Moduls / Einpassung in den Musterstudienplan:
Das Modul ist im Kontext der folgenden Studienfächer/Vertiefungsrichtungen verwendbar:

1. Informatik (Bachelor of Science)
   (Po-Vers. 2009s | weitere Pflichtmodule | Theorie der Programmierung)
2. Informatik (Bachelor of Science): 4. Semester
   (Po-Vers. 2009w | weitere Pflichtmodule | Theorie der Programmierung)
3. Mathematik (Bachelor of Science)
   (Po-Vers. 2009 | Nebenfach Informatik | Module im 2. und 3. Studienjahr | Wahlbereich 2 | Theorie der Programmierung)

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 2015, 1. Wdh.: WS 2015/2016

1. Prüfer:

Lutz Schröder

Termin: 09.10.2015, 16:30 Uhr, Ort: H 11
Termin: 15.02.2016, 11:00 Uhr, Ort: H 8 TechF