Einführung in den logisch-algebraischen Systementwurf (ELAS)
  • Wahlveranstaltung INF-BSc-312 im WiSe 2016/17 für Studierende der Bachelorstudiengänge Informatik und Angewandte Informatik
    Wahlveranstaltung im Hauptstudium der Informatik-Diplomstudiengänge für die Schwerpunktgebiete 1, 4 und 5
  • 3 SWS = 4 Credits
  • Di 12:15-13.30 und Fr 16:15-17:15 im OH 12, Raum 3.031
  • Beginn: 18. 10. 20165. 10. 2013
  • 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.
    Im einzelnen werden 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 rein funktionale ebenso wie prädikaten-, modal- und temporallogische Ansätze umfasst. Eine solche Sprache dient nicht nur der Beschreibung des jeweils modellierten Systems, sondern bestimmt auch erstens dessen Ausführung im Sinne der Auswertung von Ausdrücken und der Lösung von Gleichungen, zweitens der Verifikation von Anforderungen an das System und drittens seiner Optimierung bezüglich unterschiedlicher Zielfunktionen. Ausführung, Verifikation und Optimierung basieren auf Regelsystemen und Strategien ihrer Anwendung, die neben den o.g. semantischen Konzepten den Hauptinhalt der LV bilden.
    Als Rechnerunterstützung und Illustrationsmittel wird das interaktive Präsentations-, Test- und Beweiswerkzeug Expander2 eingesetzt. Damit lässt sich u.a. eine Brücke schlagen von der Vermittlung theoretischer Ansätze zu Anwendungs- oder Implementierungsproblemen und deren Lösungen, was umgekehrt entscheidende Kriterien für Auswahl, Anpassung und Weiterentwicklung der theoretischen Ansätze liefert.
    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 (Teile folgender Foliensätze)
  • 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
  • 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.