|
- Wahlpflichtvorlesung im WS 06/07
- 6 SWS
- Lernziel: Es werden die grundlegenden Konzepte der formalen Modellierung von Softwaresystemen vermittelt. Darüberhinaus sollen die Studierenden lernen einzuschätzen, welche mathematischen Konstruktionen und darauf aufbauenden Werkzeuge für welche Anwendungen geeignet bzw. nicht geeignet sind. Eignung bedeutet nicht nur adäquate, präzise Syntax und Semantik, sondern auch nachvollziehbares und möglichst effizientes Rechnen, Lösen und Beweisen in den jeweiligen Modellen. Da die mathematische Logik nicht nur den klarsten begrifflichen Rahmen, sondern auch die flexibelste Methodik bietet, um Softwarespezifikationen zu erstellen und zu analysieren, ist ein hinreichend souveräner Umgang mit logikbasierten Methoden ein vordringliches Lernziel.
- Inhalt (eine genaue Gliederung gibt's hier):
- Grundlegende Komponenten mathematischer Modelle zur Datenabstraktion und Systemstrukturierung: Strukturen, Unterstrukturen, Quotienten, Summen, Produkte, Relationen, Funktionen, Funktoren, Monaden
- Mehrsortige (= typisierte) Prädikatenlogik und ihre Spezialfälle: Horn- und co-Hornlogik zur relationalen Spezifikation, Gleichungslogik zur funktionalen Spezifikation
- Konzepte zur horizontalen bzw. vertikalen Strukturierung funktional-logischer Spezifikationen
- Auswertung und Verifikation durch Simplifikation (partielle Ausführung), Subsumption, Rewriting, Narrowing, Induktion und Coinduktion
- Darstellung und Animation formaler Methoden, insbesondere deduktiver Prozesse mit Hilfe von Expander2
- Skript, Haskell- und Expander2-Programme, alte Übungen und Buchempfehlungen zur LV und verwandten Themen gibt's hier.
|
|
