Korrekte Software: Grundlagen und Methoden
Vorlesungsfolien
Hier werden die Unterlagen zur Vorlesung zur Verfügung gestellt.
Die Vorlesungsfolien sind jeweils verfügbar als ganzseitiges PDF zum Betrachten, oder als 8:1 Handzettel ohne Effekte zum Drucken. Dazu die Aufzeichungen der Zoom-Sitzungen (nur verfüigbar bis zum Ende des Semesters).
- Alle Vorlesungen in einer Datei: Folien, Handzettel
- Vorlesung aus der Woche vom 13.04.21: Einführung.
Folien, Handzettel, Videos: Teil 1 Teil 2 - Vorlesung aus der Woche vom 20.04.21: Operationale Semantik.
Folien, Handzettel, Videos: Teil 1 Teil 2 - Vorlesung aus der Woche vom 27.04.21: Denotationale Semantik.
Folien, Handzettel, Videos: Teil 1 Teil 2 - Vorlesung aus der Woche vom 4/6.05.21: Äquivalenz der Operationalen und Denotationalen Semantik.
Folien, Handzettel, Videos: Teil 1 Teil 2 - Vorlesung aus der Woche vom 11/18.05.21: Die Floyd-Hoare-Logik I.
Folien, Handzettel, Videos: Teil 1 Teil 2 - Vorlesung aus der Woche vom 20.05.21: Floyd-Hoare-Logik II: Invarianten.
Folien, Handzettel, Videos: Teil 1 Teil 2 - Vorlesung aus der Woche vom 25.05.21: Korrektheit des Floyd-Hoare-Kalküls.
Folien, Handzettel, Videos: Teil 1 - Vorlesung aus der Woche vom 27.5.21 / 1.6.2021 / 3.6.2021: Strukturierte Datentypen: Strukturen und Felder.
Folien, Handzettel, Videos: Teil 1 Teil 2 Teil 3 - Vorlesung aus der Woche vom 08.06.21: Verifikationsbedingungen.
Folien, Handzettel, Videos: Teil 1 Teil 2 Teil 3 - Vorlesung aus der Woche vom 15.06.21: Vorwärts mit Floyd und Hoare.
Folien, Handzettel, Videos: Teil 1 Teil 2 - Vorlesung aus der Woche vom 22.06.21: Modellierung und Spezifikation.
Folien, Handzettel, Videos: Teil 1 Teil 2 - Vorlesung aus der Woche vom 29.06.21: Spezifikation von Funktionen.
Folien, Handzettel, Videos: Teil 1 Teil 2 - Vorlesung aus der Woche vom 06.07.21: Referenzen und Speichermodelle.
Folien, Handzettel, Videos: Teil 1 Teil 2 Teil 3 - Vorlesung aus der Woche vom 13.07.21: Rückblick \& Ausblick.
Folien, Handzettel, Videos: Teil 1
Hier sind die vorlesungsbegleitenden Unterlagen (Skriptum) in der Version vom 15.07.21
Vertiefende Lektüre
- Unsere Behandlung der operationalen und denotationalen Semantik
basiert zu großen Teilen auf diesem Buch:
- Glynn Winskel. The Formal Semantics of Programming Languages: An Introduction. The MIT Press, 1993.
- Zum Vorwärts/Rückwärtsrechnen mit den Floyd-Hoare-Regeln, und der
Berechnung von Verifikationsbedingungen:
- Forward with Hoare!, und Lecture Notes from CST (beide von Mike Gordon, University of Cambridge).