Tutorialtag 2024
Isabelle/HOL
2024-04-18 um 9:00 - 10:30 Uhr, Track 4 (online)
Dijkstra, E. W. (1970). Notes on structured programming. (EWD249).Present-day computers are amazing pieces of equipment, but most amazing of all are the uncertain grounds on account of which we attach any validity to their output.
So motivierte Dijkstra 1970 seine Betrachtungen "On the reliability of mechanisms". Viel hat sich seitdem getan: (automatisiertes) Testen gehört mittlerweile zum guten Ton, Testläufe sind in Build-Pipelines integriert, Frameworks erlauben die Generierung von Testdaten, ganze Berufszweige sind dem Testen verpflichtet. Allein, das Korollar, mit dem die oben zitierten Betrachtungen enden, hat Bestand: Testen kann nur die An-, nie aber die Abwesenheit, von Fehlern aufzeigen.
Wollen wir mehr, brauchen wir mehr: Geht es darum, die Korrektheit von Systemen zu untersuchen oder gar nachzuweisen, sind Model-Checker, Theorembeweiser – kurz: formale Methoden – gefragt. Auf den ersten Blick mag funktionale Korrektheit vor diesem Hintergrund als weißer Wal erscheinen: Formale Methoden sind voraussetzungsreich, oftmals kostspielig und im Ergebnis nicht immer befriedigend. Doch sie haben ihren Platz und so laden wir alle Neugierigen ein, uns auf die Pequod zu folgen und nach Moby Dick Ausschau zu halten.
Anhand eines kleinen, aber nicht-trivialen Beispiels machen wir uns mit dem Beweisassistenten Isabelle vertraut. Wir werden Mergesort implementieren, gemeinsam überlegen, was Korrektheit in diesem Fall bedeutet, und uns schließlich daran machen, die Richtigkeit unserer Implementierung zu beweisen.
Wer der Live-Coding-Session auf dem eigenen Rechner folgen will benötigt Isabelle: Installationsanleitungen.
Dann mal Mast- und Schotbruch! Wir sehen uns im Krähennest 🐋
Auf Track 4 gehts weiter mit: Nix from Scratch.
