inf450 - Korrektheit von Graphprogrammen (Vollständige Modulbeschreibung)

inf450 - Korrektheit von Graphprogrammen (Vollständige Modulbeschreibung)

Originalfassung Englisch PDF Download
Modulbezeichnung Korrektheit von Graphprogrammen
Modulkürzel inf450
Kreditpunkte 6.0 KP
Workload 180 h
Einrichtungsverzeichnis Department für Informatik
Verwendbarkeit des Moduls
  • Master Informatik (Master) > Theoretische Informatik
Zuständige Personen
  • Lehrenden, Die im Modul (Modulverantwortung)
  • Lehrenden, Die im Modul (Prüfungsberechtigt)
Teilnahmevoraussetzungen
- inf400 Theoretische Informatik I
- inf401 Theoretische Informatik II
Kompetenzziele
Modellierung von Systemen, Systemveränderungen und Systemeigenschaften. Einführung in Graphprogramme und Grapheigenschaften. Einführung in die Korrektheit von Systemen. Methoden zum Nachweis von Korrektheit von Systemen.
Fachkompetenzen
Die Studierenden:
  • beschreiben die Grundlagen von Graphprogrammen und Grapheigenschaften
  • beschreiben Verfahren zum Nachweis von Korrektheit
Methodenkompetenzen
Die Studierenden:
  • modellieren Systeme, Systemveränderungen und Systemeigenschaften
  • wenden Graphprogamme an
Sozialkompetenzen
Die Studierenden:
  • lösen Problemstellungen im Team
  • präsentieren Lösungsvorschläge und diskutieren diese
Selbstkompetenzen
Die Studierenden:
  • reflektieren ihr Handeln und beziehen dabei Graphprogramme und Grapheigenschaften ein
Modulinhalte
Die Veranstaltung führt in die Modellierung von Systemen, Systemveränderungen und Systemeigenschaften mit Hilfe von Graphen, Graphprogrammen und Graphbedingungen ein und stellt eine Methode zum Nachweis der Korrektheit von Systemen bzgl. einer Vor- und Nachbedingung vor. Die zugrundeliegenden Strukturen in der Veranstaltung sind Graphen; sie werden in praktisch allen Bereichen der Informatik benutzt, um komplexe Strukturen darzustellen. Graphprogramme sind mit Hilfe der Kernkonstrukte nichtdeterministische Anwendung einer Regel, sequentielle Komposition und Iteration aufgebaut und erlauben eine programmgesteuerte Veränderung der aktuellen Graphstruktur. Eine wohlbekannte Methode zur Bestimmung der Korrektheit von Programmen bezüglich einer Vor- und Nachbedingung basiert auf der Konstruktion einer schwächsten Vorbedingung des Programms bzgl. der Nachbedingung und dem Versuch zu entscheiden, ob die Vorbedingung die schwächste Vorbedingung impliziert.
Literaturempfehlungen
  • A. Habel, K.-H. Pennemann. Correctness of high-level transformation systems relative to nested conditions. Mathematical Structures in Computer Science, 19:245-296, 2009.
  • A. Habel, K.-H. Pennemann, A. Rensink. Weakest preconditions for high-level programs. In Graph Transformations (ICGT 2006), LNCS 4178, 445-460, 2006.
  • K. Azab, A. Habel, K.-H. Pennemann, C. Zuckschwerdt. ENFORCe: A system for ensuring formal correctness of high-level programs. In Electronic Communications of the EASST, Vol. 1. 82-93, 2007.
Links
Unterrichtssprache Deutsch
Dauer in Semestern 1 Semester
Angebotsrhythmus Modul im 2-Jahres-Zyklus
Aufnahmekapazität Modul unbegrenzt
Hinweise
Wird oft als Blockveranstaltung angeboten
Lehr-/Lernform 1VL + 1Ü
Vorkenntnisse - inf400 Theoretische Informatik I
- inf401 Theoretische Informatik II
Lehrveranstaltungsform Kommentar SWS Angebotsrhythmus Workload Präsenz
Vorlesung 3 WiSe 42
Übung 1 WiSe 14
Präsenzzeit Modul insgesamt 56 h
Prüfung Prüfungszeiten Prüfungsform
Gesamtmodul
Werden in der Veranstaltung bekannt gegeben
Fachpraktische Übungen und mündliche Prüfung