Korrekte Software: Grundlagen und Methoden
Vorlesungsfolien
Die Vorlesungsfolien sind jeweils verfügbar als ganzseitiges PDF zum Betrachten, oder als 8:1 Handzettel ohne Effekte zum Drucken:
- Vorlesung vom 03.04.24 — Einführung: Folien, Handzettel
- Vorlesung vom 10.04.24 — Operationale Semantik: Folien, Handzettel
- Vorlesung vom 17.04.24 — Denotationale Semantik: Folien, Handzettel
- Vorlesung vom 24.04.24 — Äquivalenz der Operationalen und Denotationalen Semantik: Folien, Handzettel
- Vorlesung vom 02.05.24 — Die Floyd-Hoare-Logik: Folien, Handzettel
- Alle Vorlesungen in einer Datei: Folien Handzettel
- Vorlesungsnotizen in der Fassung vom 15.05.24: Notes
Hier sind die Gruppenarbeitsblätter im HackMD.
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).