Modulnummer

Modulbezeichnung

Titel (englisch)

Pflicht/Wahl

Erklärung

CP

Berechnung des Workloads

Turnus

Dauer

Form

Prüfung

Anforderungen

Lernziele

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.

Lerninhalte

• 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);

Quellen

Sprache

Bemerkung

Zuletzt geändert