Bedeutung und Korrektheit von C Programmen

Willkommen auf der Heimatseite der Lehrveranstaltung "Bedeutung und Korrektheit von C Programmen" im Sommersemester 2008!

Thema der Veranstaltung ist die Verifikation von imperativen Programmen in der Programmiersprache C. Wir werden anhand des Standards ISO C 9899:1999 einen Begriff der formalen Bedeutung von C Programmen entwickeln, und zeigen, wie damit Beweise von Programmeigenschaften geführt werden können.

Gliederung

Teil I: Die Sprache C
- Einführung in den C-Standard 9899:1999
- Lexikalik und Grammatik
- Das C-Typsystem
- Speichermodell, Pointer & Arrays
Teil II: Die Bedeutung von C-Programmen
- Bedeutung von Anweisungen
- Das Speichermodell formal
- Bedeutung von Ausdrücken
Teil III: Beweis von Programmeigenschaften
- Erinngerungen an Floyd-Hoare
- Der Floyd-Hoare-Kalkül für C
- Berechnung von Verifikationsbedingungen

Organisatorisches

Die Veranstalter sind Lutz Schröder und Christoph Lüth.

VAK: 03-05-H-706.09 .
K 4 SWS (6 ECTS) Praxis (A), Handelsklasse: I

Termine:

Di, 10:00 - 12:00, MZH 4194
Mi, 13:00 - 15:00, MZH 7210

Vorlesungsmaterialien

Im folgenden sind die PDF-Versionen in Originalgröße zum Betrachten, und die PS-Versionen zum Ausdrucken 8:1 verkleinert.

Vorlesung vom 07.04.08: [PDF] [PS]
Vorlesung vom 15.04.08: [PDF] [PS]
Dazu: permute.c
Vorlesung vom 22.04.08: [PDF] [PS]
Vorlesung vom 29.04.08: [PDF] [PS]
Vorlesung vom 02.07.08: [PDF] [PS]
Vorlesung vom 08.07.08: [PDF] [PS]

Die Materialen für die Vorlesung vom 06.05 bis zum 25.06:

[PDF] (Fassung vom 22.07.08).

Für die Teilnehmer, die sich für eine mündliche Prüfung entschlossen haben:

Der Fragenkatalog (Fassung vom 22.07.08).

Übungsblätter

Übungsblatt 1 vom 16.04.08.
- Dazu das Beispiel: very-simple.y.
  Übersetzen mit yacc very-simple.y; gcc y.tab.c -ly.
  Siehe auch die Links unten
- Das einfache Beispiel mit lex und yacc.
- Die Grammatik für C
Übungsblatt 2 vom 24.06.08.

Links und Literatur

Die Programmiersprache C

ISO IEC: C - Approved standards, dort insbesondere eine frei verfügbare, vorläufige (aber fast endgültige) Fassung des Standards 9899 (PDF)
Der Klassiker:
Brian Kernighan, Dennis Ritchie: The C Programming Language. Prentice-Hall, 1988
Gut zu lesen und sehr gründlich, stellenweise etwas geschwätzig:
Peter van der Linden: Expert C Programming (Deep C Secrets). SunSoft Press, prentice-Hall, 1994.
Kurz, knapp und lesenswert, aber etwas angestaubt:
Andrew Koenig: C Traps and Pitfalls, Addison-Wesley, 1989.
Ein Online-Buch. Umsonst, aber dafür nicht schlechter:
Mike Banahan, Declan Brady and Mark Doran: The C Book. Addison-Wesley, 1991.

Parser

Das Drachenbuch (auch ein Klassiker):
Aho, Sethi, Ullman: Compilerbau, Addison-Wesley.
Eine Seite zu Lex und Yacc
Happy: Yacc für Haskell