Über die Veranstaltung

In dieser Veranstaltung geht es um eine der Kernfragen der Informatik: wie schreiben wir korrekte Programme?

Dazu werden wir den Hoare-Kalkül kennenlernen, und näher betrachten. Wir werden die Frage klären, was so ein Programm eigentlich macht (was ist seine Semantik), und wie können wir beweisen, dass es das tut, was es soll.

Wir werden dazu eine Sprache C0 betrachten, bei der es sich um eine Untermenge der beliebten Prorgammiersprache C handelt (ohne deren problematischere Anteile). Wir werden dazu den Hoare-Kalkül, wie wir ihn in Lehrbüchern (oder der Wikipedia) finden, um interessante Aspekte einer echten Programmiersprache wie Referenzen, strukturierte Datentypen, Funktionen und Prozeduren, erweitern.

Die Übungen werden diese Konzepte sowohl theoretisch als auch praktisch erkunden; dabei werden wir in der funktionalen Sprache Scala ein Werkzeug implementieren, das uns erlaubt, mit dem Theorembeweiser Isabelle die Korrektheit unserer Programme mechanisch zu zeigen.