Programmverifikation

Inhaltsverzeichnis1 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.