Programmverifikation

1 Einführung.- 1.1 Beispiel eines parallelen Programmes.- Lösung 1.- Lösung 2.- Lösung 3.- Lösung 4.- Lösung 5.- Lösung 6.- 1.2 Programmkorrektheit.- 1.3 Struktur dieses Buches.- 2 Vorbereitungen.- 2.1 Syntax.- 2.2 Getypte Ausdrücke.- Typen.- Variablen.- Konstanten.- Ausdrücke.- Indizierte Variablen.- 2.3 Semantik von Ausdrücken.- Feste Struktur.- Zustände.- Definition der Semantik.- Modifikation von Zuständen.- 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.- Eigenschaften der Semantiken.- 3.3 Verifikation.- Partielle Korrektheit.- Totale Korrektheit.- Korrektheit der Beweissysteme.- 3.4 Beweisskizzen.- Partielle Korrektheit.- Totale Korrektheit.- Programmdokumentation.- 3.5 Vollständigkeit.- 3.6 Zusätzliche Axiome und Regeln.- 3.7 Systematische Entwicklung korrekter Programme.- Summations-Problem.- 3.8 Fallstudie: Minimale Abschnittssumme.- 3.9 Übungsaufgaben.- 3.10 Bibliographische Anmerkungen.- 4 Disjunkte parallele Programme.- 4.1 Syntax.- 4.2 Semantik.- Determinismus.- Sequentialisierung.- 4.3 Verifikation.- Parallele Komposition.- Hilfsvariablen.- Korrektheit der Beweissysteme.- 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.- Atomarität.- 5.4 Verifikation: Partielle Korrektheit.- Komponenten-Programme.- Keine Kompositionalität des Ein/Ausgabe-Verhaltens.- Parallele Komposition: Interferenz-Freiheit.- Notwendigkeit von Hilfsvariablen.- Korrektheit des Beweissystems.- 5.5 Verifikation: Totale Korrektheit.- Komponenten-Programme.- Parallele Komposition: Interferenz-Freiheit.- Korrektheit des Beweissystems.- Diskussion.- 5.6 Fallstudie: Finde positives Element schneller.- 5.7 Verändern von Interferenzpunkten.- 5.8 Fallstudie: Parallele Nullstellensuche.- Schritt 1. Vereinfachung des Programms.- Schritt 2. Beweis der partiellen Korrektheit.- 5.9 Übungsaufgaben.- 5.10 Bibliographische Anmerkungen.- 6 Parallele Programme mit Synchronisation.- 6.1 Syntax.- 6.2 Semantik.- 6.3 Verifikation.- Partielle Korrektheit.- Korrektheit des Beweissystems.- Schwache totale Korrektheit.- Totale Korrektheit.- Korrektheit des Beweissystems.- 6.4 Fallstudie: Erzeuger/Verbraucher-Problem.- 6.5 Fallstudie: Wechselweiser Ausschluß.- Formulierung des Problems.- Verifikation.- Peterson’s Lösung.- Dijkstra’s Lösung.- 6.6 Verändern von Interferenzpunkten.- 6.7 Fallstudie: Synchronisierte Nullstellensuche.- Schritt 1. Vereinfachung des Programms.- Schritt 2. Zerlegung der Verifikationsaufgabe.- Schritt 3. Beweis der Terminierung.- Schritt 4. Beweis der partiellen Korrektheit.- 6.8 Übungsaufgaben.- 6.9 Bibliographische Anmerkungen.- 7 Nichtdeterministische Programme.- 7.1 Syntax.- 7.2 Semantik.- Eigenschaften der Semantiken.- 7.3 Vorteile nichtdeterministischer Programme.- Symmetrie.- Laufzeitfehler.- Nichtdeterminismus.- Modellierung von Parallelität.- 7.4 Verifikation.- 7.5 Fallstudie: Wohlfahrtsbetrüger.- 7.6 Transformation paralleler Programme.- 7.7 Übungsaufgaben.- 7.8 Bibliographische Anmerkungen.- 8 Verteilte Programme.- 8.1 Syntax.- Sequentielle Prozesse.- Verteilte Programme.- 8.2 Semantik.- 8.3 Transformation verteilter Programme.- Semantische Beziehung zwischen S und T(S).- 8.4 Verifikation.- Partielle Korrektheit.- Schwache Totale Korrektheit.- Totale Korrektheit.- Beweissysteme.- 8.5 Fallstudie: Übertragungsproblem.- Schritt 1. Zerlegung der Verifikationsaufgabe.- Schritt 2. Partielle Korrektheit.- Schritt 3. Kein Laufzeitfehler und keine Divergenz.- Schritt 4. Deadlock-Freiheit.- 8.6 Übungsaufgaben.- 8.7 Bibliographische Anmerkungen.- A. Semantik.- B. Beweisregeln.- C. Beweissysteme.- D. Beweisskizzen.- Autorenverzeichnis.- Stichwortverzeichnis.- Symbolverzeichnis.