Korrekte Software

Jährlich

Ziel der Veranstaltung ist es, die Grundbegriffe der korrekten Softwareentwicklung zu verstehen. Wie können wir Software schreiben, die tut was sie soll? Und wie können wir das beweisen?

Dazu betrachten wie die Grundbegriffe der formalen Semantik und der Floyd-Hoare-Logik. Lernziel ist es, Eigenschaften von einfachen C-Programmen spezifizieren und beweisen zu können, und zu verstehen, wie diese Techniken auf reale C-Programme (oder andere Programmiersprachen) skalieren können.

• Logische Grundlagen: Formale Logik, Prädikatenkalkül, Vollständigkeit und Korrektheit;

• Grundlagen der Floyd-Hoare-Logik;

• Operationale Semantik für eine einfach imperative Programmiersprache;

• Vollständigkeit und Korrektheit der Floyd-Hoare-Logik für diese Sprache;

• Erweiterung der Logik um Funktionsaufrufe, strukturierte Datentypen und Referenzen (Zeiger);