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]
- [PDF] (Fassung vom 22.07.08).
- 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
- Dazu das Beispiel: very-simple.y.
- Ü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