Programmverifikation

Inhaltsverzeichnis

• 1 Einführung.
• 1.1 Beispiel eines parallelen Programmes.
• 1.2 Programmkorrektheit.
• 1.3 Struktur dieses Buches.
• 2 Vorbereitungen.
• 2.1 Syntax.
• 2.2 Getypte Ausdrücke.
• 2.3 Semantik von Ausdrücken.
• 2.4 Formale Beweissysteme.
• 2.5 Logische Formeln.
• 2.6 Semantik von logischen Formeln.
• 2.7 Substitution.
• 2.8 Substitutions-Lemma.
• 2.9 Übungsaufgaben.
• 2.10 Bibliographische Anmerkungen.
• 3 Deterministische Programme.
• 3.1 Syntax.
• 3.2 Semantik.
• 3.3 Verifikation.
• 3.4 Beweisskizzen.
• 3.5 Vollständigkeit.
• 3.6 Zusätzliche Axiome und Regeln.
• 3.7 Systematische Entwicklung korrekter Programme.
• 3.8 Fallstudie: Minimale Abschnittssumme.
• 3.9 Übungsaufgaben.
• 3.10 Bibliographische Anmerkungen.
• 4 Disjunkte parallele Programme.
• 4.1 Syntax.
• 4.2 Semantik.
• 4.3 Verifikation.
• 4.4 Fallstudie: Finde Positives Element.
• 4.5 Übungsaufgaben.
• 4.6 Bibliographische Anmerkungen.
• 5 Parallele Programme mit gemeinsamen Variablen.
• 5.1 Zugriff auf gemeinsame Variablen.
• 5.2 Syntax.
• 5.3 Semantik.
• 5.4 Verifikation: Partielle Korrektheit.
• 5.5 Verifikation: Totale Korrektheit.
• 5.6 Fallstudie: Finde positives Element schneller.
• 5.7 Verändern von Interferenzpunkten.
• 5.8 Fallstudie: Parallele Nullstellensuche.
• 5.9 Übungsaufgaben.
• 5.10 Bibliographische Anmerkungen.
• 6 Parallele Programme mit Synchronisation.
• 6.1 Syntax.
• 6.2 Semantik.
• 6.3 Verifikation.
• 6.4 Fallstudie: Erzeuger/Verbraucher-Problem.
• 6.5 Fallstudie: Wechselweiser Ausschluß.
• 6.6 Verändern von Interferenzpunkten.
• 6.7 Fallstudie: Synchronisierte Nullstellensuche.
• 6.8 Übungsaufgaben.
• 6.9 Bibliographische Anmerkungen.
• 7 Nichtdeterministische Programme.
• 7.1 Syntax.
• 7.2 Semantik.
• 7.3 Vorteile nichtdeterministischer Programme.
• 7.4 Verifikation.
• 7.5 Fallstudie: Wohlfahrtsbetrüger.
• 7.6 Transformationparalleler Programme.
• 7.7 Übungsaufgaben.
• 7.8 Bibliographische Anmerkungen.
• 8 Verteilte Programme.
• 8.1 Syntax.
• 8.2 Semantik.
• 8.3 Transformation verteilter Programme.
• 8.4 Verifikation.
• 8.5 Fallstudie: Übertragungsproblem.
• 8.6 Übungsaufgaben.
• 8.7 Bibliographische Anmerkungen.
• A. Semantik.
• B. Beweisregeln.
• C. Beweissysteme.
• D. Beweisskizzen.
• Autorenverzeichnis.
• Stichwortverzeichnis.
• Symbolverzeichnis.