Programmverifikation

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.