Programmverifikation

Sequentielle, parallele und verteilte Programme
1994
ISBN: 978-3-540-57479-8
Verlag: Springer Berlin Heidelberg

Buch, Deutsch, 258 Seiten, Format (B × H): 155 mm x 235 mm, Gewicht: 417 g

Reihe: Springer-Lehrbuch

Dieses Buch bietet als erstes Lehrbuch eine systematische
Einf}hrung in die Programmverifikation. Sequentielle,
parallele und verteilte Programme werdenin einheitlicher
Weise behandelt.
In den einzelnen Kapiteln des Buches werden deterministische
und nichtdeterministische Programme, Programme mit
gemeinsamen Variablen und verteilte Programme mit
Kommunikation }berBotschaftenaustausch behandelt. F}r jede
dieser Programmklassen werden eine operationelle Semantik,
Syntax-gerichtete Verifikationsregeln mitsamt
Korrektheitsbeweis und ein gr ~eres Verifikationsbeispiel
vorgestellt. Insbesondere werden Programme zur L sung der
klassischen Probleme Erzeuger-Verbraucher, wechselweiser
Ausschlu~ und verteilte Terminierung diskutiert und
verifiziert. Eine Besonderheit desBuches ist die
einheitliche Behandlung von Fairne~-Annahmen und die
Benutzung von Programmtransformationen.
Das Buch eignet sich f}r ein- oder zweisemestrige
Vorlesungen }ber Programmverifikation. Die Kapitel sind
einheitlich strukturiert und enthalten eine Reihe von
]bungsaufgaben und bibliographischen Hinweisen. Das Buch
f}hrt auch an aktuelle Themen der Forschung heran.

Zielgruppe

Research

Autoren/Hrsg.

Olderog, Ernst-Rüdiger

Apt, Krzysztof R.

Fachgebiete

• Mathematik | Informatik Mathematik Mathematik Allgemein Grundlagen der Mathematik
• Mathematik | Informatik EDV | Informatik Informatik Rechnerarchitektur
• Mathematik | Informatik EDV | Informatik Programmierung | Softwareentwicklung Programmierung: Methoden und Allgemeines
• Mathematik | Informatik EDV | Informatik Informatik Logik, formale Sprachen, Automaten
• Mathematik | Informatik EDV | Informatik Daten / Datenbanken Zeichen- und Zahlendarstellungen

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.