Allgemeine Informationen
| Veranstaltungsname | Vorlesung: 2.01.450 Korrektheit von Graphprogrammen |
| Untertitel | inf450 |
| Veranstaltungsnummer | 2.01.450 |
| Semester | WiSe18/19 |
| Aktuelle Anzahl der Teilnehmenden | 4 |
| erwartete Teilnehmendenanzahl | 20 |
| Heimat-Einrichtung | Department für Informatik |
| Veranstaltungstyp | Vorlesung in der Kategorie Lehre |
| Erster Termin | Freitag, 26.10.2018 13:00 - 16:00, Ort: A02 2-239 |
| Art/Form | Blockveranstaltung 3V+1Ü |
| Lehrsprache | deutsch |
| Sonstiges |
Die LV 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 LV sind Graphen; sie werden in praktisch allen Bereichen der Informatik benutzt, um komplexe Strukturen darzustellen. Graphprogramme sind mit Hilfe der Kernkonstrukte nichtdeterministische Regelanwendung, sequentielle Komposition und Iteration aufgebaut und erlauben eine programmgesteuerte Veränderung der aktuellen Graphstruktur. Es zeigt sich, dass Graphprogramme berechnungsvollständig sind. Eine wohl-bekannte 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 (siehe z.B. [Dijkstra 76]). Zum Ableiten der Korrektheit der Spezifikationen werden auch Beweiskalküle [Hoare, 1983] herangezogen. |
