Funktionallogisches Modellieren und Programmieren (FLMP)
morphdragon
  • Vertiefungsmodul INF-MSc-331 im Wintersemester 2023/24
  • 4 SWS - 6 Credits
  • Vertiefungsmodul in den Masterstudiengängen Informatik und Angewandte Informatik
    Forschungsbereich Software, Sicherheit und Verifikation
  • Dozent und Übungsleiter: Prof. Dr. Peter Padawitz
  • Termin: Di 14:15-17:30 im OH 12, Raum 1.054
  • Beginn: 10. 10. 2023
  • Bitte über LSF im Moodle-Arbeitsraum zur LV anmelden.
  • Inhalt: Die LV behandelt grundlegende Konzepte zu Konstruktion, Ausführung und Verifikation formaler Modelle. 50 Jahre Forschung und Entwicklung an der Schnittstelle zwischen Mathematik und Softwaretechnik haben gezeigt, dass Aufbau und Verhalten der Objekte eines formalen Modells von spezifischen Konstruktoren bzw. Destruktoren bestimmt werden. Konstruktormengen werden induktiv als Grammatiken o.ä. definiert. Destruktormengen bestehen aus Transitions- und Attributfunktionen zustandsbasierter Systeme (Automaten, Kripke-Strukturen, Petri-Netze, Flussgraphen, Prozessalgebren, Klassenhierarchien, etc.) und werden heute oft coinduktiv definiert. Beide Modelltypen verfügen über mächtige Auswertungs-, Lösungs- und Beweismethoden. Die LV wird zunächst fundamentale typ- und kategorientheoretische Konzepte (Funktoren, Limiten, Algebren, Folds, Unfolds, Monaden) behandeln und darauf aufbauend eine an Haskell, Prolog und SQL angelehnte funktionallogische Sprache, die im interaktiven Spezifikationswerkzeug Expander2/3 ausführbar ist.
  • Kompetenzen: Die Studierenden lernen, welche grundlegenden mathematischen Konstrukte inkl. Entwurfsmuster und Beweisverfahren für welche Anwendungen geeignet sind und wie sie an dortige Anforderungen angepasst werden können. Anstatt gängige formale Methoden getrennt voneinander zu betrachten, werden alle behandelten Anwendungen in einer einzigen, aber mächtigen und flexiblen funktionallogischen Sprache formuliert. So wird der souveräne Umgang mit logisch-algebraischen Techniken gefördert, der nicht nur bei der Synthese oder Analyse von Programmen weiterhilft, sondern auch bei der Auswahl für die jeweilige Anwendung geeigneter Entwurfs- und Programmierwerkzeuge.
  • Materialien