Einführung in den logisch-algebraischen Systementwurf (ELAS)
- Dozent und Übungsleiter: Prof. Dr. Peter Padawitz
- Wahlveranstaltung INF-BSc-312 im WiSe 2018/19 für Studierende der Bachelorstudiengänge Informatik und Angewandte Informatik sowie Wahlveranstaltung im Hauptstudium der Informatik-Diplomstudiengänge für die Schwerpunktgebiete 1, 4 und 5
- 3 SWS = 4 Credits
- Zur Teilnahme bitte unter Moodle-Seite dieser LV anmelden.
- Di 14:15-16.30 im OH 12, Raum 3.031
- Beginn: 9. 10. 2018
- Inhalt: Die LV behandelt die grundlegenden Konzepte zu Konstruktion, Ausführung und Verifikation formaler Modelle. 40 Jahre Forschung und Entwicklung an der Schnittstelle zwischen Mathematik und Softwaretechnik haben zu der heutigen Sicht geführt, nach der jedes Modell konstruktor- oder destruktorbasiert ist, sich über den Aufbau oder das Verhalten seiner Objekte definiert. Zur ersten Gruppe von Modellen gehören all diejenigen, deren Elemente aus endlich vielen Komponenten bestehen und die i.d.R. durch Grammatiken beschrieben werden. Die zweite Gruppe umfasst Automaten, Kripke-Strukturen, Petri-Netze, Berechnungssequenzen, Term- und Flussgraphen, Prozessalgebren, Klassenhierarchien, kurzum alle durch Zustandsübergänge und/oder Attribute charakterisierten Strukturen. Theoretische Untersuchungen ebenso wie praktische Anwendungen haben gezeigt, dass beide Modellklassen dual zueinander sind und diese Dualität von der Datenstrukturierung bis zu den Rechen- und Beweismethoden reicht.
Nach einer Wiederholung der mengentheoretischen Strukturierungskonzepte Produkt, Summe Quotient und Teilmenge - u.a. diese Konzepte verallgemeinernde - Grundbegriffe der Kategorientheorie eingeführt: Kategorien, Funktoren, natürliche Transformationen, Limiten, Colimiten, Algebren, Coalgebren, freie und cofreie Strukturen. In den Kategorien mehrsortiger Mengen bzw. CPOs (Mengen mit kettenvollständiger Halbordnung) bilden diese Konstruktionen die semantische Grundlage für eine universelle Spezifikationssprache, die sowohl funktionale als auch relationale Ansätze umfasst. Eine solche Sprache dient nicht nur der Beschreibung des jeweils modellierten Systems, sondern bestimmt auch dessen Ausführung im Sinne der Auswertung von Ausdrücken, der Lösung von Gleichungen, der logischen Ableitung von Eigenschaften, etc. Die Ausführung basiert auf Regelsystemen und Strategien ihrer Anwendung, die neben den o.g. semantischen Konzepten den Hauptinhalt der LV bilden.
- Kompetenzen: Die Studierenden lernen einzuschätzen, welche mathematischen Konstruktionen und darauf aufbauenden Werkzeuge für welche Anwendungen geeignet bzw. nicht geeignet sind und wie man sie an spezielle Anforderungen anpassen kann. Eignung entsteht nicht nur durch eine adäquate, präzise Syntax und Semantik, sondern auch durch den Einsatz von Methoden, die nachvollziehbares und möglichst effizientes Rechnen, Lösen und Beweisen in den jeweiligen Modellen ermöglichen. Da Logik und Algebra nicht nur den klarsten begrifflichen Rahmen, sondern auch die mächtigsten und flexibelsten Verfahren bieten, um Softwarespezifikationen zu erstellen und zu analysieren, ist der hinreichend souveräne Umgang mit logisch-algebraischen Techniken ein vordringliches Lernziel.
- Materialien
- Einführungen in Kategorientheorie
(Bei Interesse an Kopien bitte Peter Padawitz anschreiben)
- David Spivak, Category Theory for the Sciences, MIT Press 2014; alte pdf-Version
- Michael Barr, Charles Wells, Category Theory, Lecture Notes 1999
- R.F.C. Walters, Categories and Computer Science, Cambridge University Press 1992
- Benjamin C. Pierce, Basic Category Theory for Computer Scientists, MIT Press 1991
- Michael Arbib, Ernest Manes, Arrows, Structures, and Functors, Academic Press 1975
- Ehrig, Mahr, Cornelius, Große-Rhode, Zeitz, Mathematisch-strukturelle Grundlagen der Informatik, Springer 2001
(gibt's in der Lehrbuchsammlung)
- Weitere Literatur sowie Infos zu Inhalten der LV stehen in den Ankündigungen der Vorgängerveranstaltungen Zustandsbasierte Systeme und versteckte Datentypen und Formale Methoden des Systementwurfs.