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 vom 19.04.22 — Einführung: Folien, Handzettel
- Vorlesung vom 26.04.22 — Operationale Semantik: Folien, Handzettel
- Vorlesung vom 05.05.22 — Denotationale Semantik: Folien, Handzettel
- Vorlesung vom 10.05.22 — Äquivalenz der Operationalen und Denotationalen Semantik: Folien, Handzettel
- Vorlesung vom 17.05.22 — Die Floyd-Hoare-Logik I: Folien, Handzettel
- Vorlesung vom 24.05.22 — Floyd-Hoare-Logik II: Invarianten: Folien, Handzettel
- Vorlesung vom 02.06.22 — Korrektheit des Floyd-Hoare-Kalküls: Folien, Handzettel
- Vorlesung vom 07.06.2022 — Strukturierte Datentypen: Strukturen und Felder: Folien, Handzettel
- Vorlesung vom 14.06.22 — Verifikationsbedingungen: Folien, Handzettel
- Vorlesung vom 21.06.22 — Vorwärts mit Floyd und Hoare: Folien, Handzettel
- Vorlesung vom 28.06.22 — Funktionen und Prozeduren I: Folien, Handzettel
- Vorlesung vom 05.07.22 — Funktionen und Prozeduren II: Folien, Handzettel
- Vorlesung vom 12.07.22 — Referenzen und Speichermodelle: Folien, Handzettel
- Vorlesung vom 21.07.21 — Rückblick \& Ausblick: Folien, Handzettel
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).