zurück zur Startseite der Softwaretechnik-Trends , zu Band 15 Heft 1


     Buchbesprechung



K.R. Apt, E.-R. Olderog: Programmverifikation, Springer-Verlag, 1994, 258 S., ISBN 3-540-57479-4


CR-Klassifikation: D.1.3-4, D.2.4, D.3.1, D.4.1, F.3.1-3

Schlüsselwörter: Programmverifikation, deterministische / nichtdeterministische sequentielle Programme, parallele Programme, verteilte Programme


Das Buch bietet eine Einführung in die Problematik der Programmverifikation. Der Schwerpunkt liegt auf der Darstellung möglicher Fehlersituationen, die bei der Entwicklung verschiedener Programmklassen entstehen können, und wie die Entwicklung korrekter Programme formal durch die Technik der Programmverifikation gesichert werden kann. Das Buch wendet sich mit dieser Ausrichtung an Studenten der Informatik im Hauptstudium. Die deutsche Übersetzung ist gegenüber der englischen Originalfassung von 1991 um die Aspekte Fairneß und verteilte Terminierung gekürzt und umfaßt nun vom Umfang den Stoffinhalt einer vierstündigen einsemestrigen Vorlesung.

Korrektheit ist ein bedeutender Qualitätsfaktor bei der Entwicklung von Programmen. Das Buch beginnt mit einer Veranschaulichung von möglichen Fehlersituationen und Maßnahmen zur Sicherung der Korrektheit an einem Beispiel. Die zum Verständnis von Programmiersprachen und Logik notwendigen Grundlagen werden in knapper Form angegeben. Die Semantik der Programme wird mit Hilfe der für parallele oder verteilte Programme üblichen strukturell operationalen Semantik definiert. Begriffe wie Interpretation einer Spezifikationslogik und Grundelemente von Beweissystemen werden kurz eingeführt. In den folgenden Abschnitten werden Verifikationstechniken für verschiedene Programmklassen behandelt. Zu diesen gehören deterministische sequentielle, disjunkte parallele, parallele mit gemeinsamen Variablen, parallele mit Synchronisation, nichtdeterministische und verteilte Programme. Der Schwerpunkt dieses Buches liegt auf den parallelen und verteilten Programmen. Daher werden diese auch schrittweise in mehreren Programmklassen eingeführt, die dem gegenüber sequentiellen Programmen erschwerten Verständnis solcher Programme Rechnung tragen. Die sequentiellen Programme werden nur soweit betrachtet, wie sie für das Verständnis weiterer Sprachklassen notwendig sind. Jedes Kapitel, das eine Programmklasse beschreibt, umfaßt eine informelle und formale Definition der Sprachklasse, ein Beweissystem, eine oder mehrere Fallstudien, sowie Übungsaufgaben und bibliographische Hinweise. Für jede Programmklasse werden Beweissysteme zur partiellen und totalen Korrektheit des Ein-/Ausgabeverhaltens angegeben; für parallele und verteilte Programme wird der Begriff der schwachen totalen Korrektheit eingeführt. Konsistenz und für eine Programmklasse exemplarisch auch Vollständigkeit dieser Beweissysteme werden gezeigt. Die Fallstudien behandeln übliche Problemstellungen aus den jeweiligen Programmklassen, wie den wechselseitigen Ausschluß oder das Erzeuger/Verbraucher-Problem. Es werden zudem Aspekte wie die systematische Programmentwicklung nach Dijkstra und Gries oder Programmtransformation behandelt. Für die gestellten Aufgaben werden keine Lösungen angeboten. Der Anhang faßt Programmsemantiken, Beweissysteme und Beweisskizzen zusammen.

Die bibliographischen Hinweise sind gegenüber der Originalversion des Buches aktualisiert und bieten somit einen guten Überblick über alle weitergehenden Aspekte der Programmverifikation bis hin zu aktuellsten Entwicklungen. In den bibliographischen Hinweisen werden auch alternative Ansätze beleuchtet. Etwa wird die Synchronisation paralleler Programme über das await -Konstrukt nach Owicki und Gries definiert. Vor- und Nachteile gegenüber dem Hoare'schen Semaphor-Ansatz werden diskutiert.

Dieses Buch ist das erste deutschsprachige, das den Komplex paralleler und verteilter Programmierung aus Sicht der Verifikation aufarbeitet. Andere Bücher, wie das 1989 bei Hanser in deutscher Übersetzung erschienene Programmkonstruktion und Verifikation von R. Backhouse, Programmentwicklung und Verifikation von G. Futschek (ebenfalls 1989 bei Springer erschienen) oder Einführung in die Programmverifikation von B. Hohlfeld und W. Struckmann (1992 im BI-Wissenschaftsverlag erschienen), legen ihren Schwerpunkt auf die Betrachtung deterministischer, sequentieller Programme. Im englischsprachigen Bereich ist das Buch in bezug auf die inhaltliche Ausrichtung mit Program Verification von N. Franchez (erschienen 1992 bei Addison-Wesley) vergleichbar.

Zusammenfassend ist das Buch eine gut lesbare und gut motivierende, insgesamt also gelungene Einführung in die Thematik. Die formale Aufarbeitung des Bereiches ist nicht die Zielsetzung des Buches, ist aber, soweit sie erfolgt, -- wie bei den Autoren nicht anders zu erwarten -- klar und präzise dargestellt. Das Buch richtet sich zwar in erster Linie an Einsteiger in den Bereich Verifikation, und setzt außer einem grundlegenden Verständnis von Programmiersprachen und mathematischem Grundwissen keine konkreten Kenntnisse voraus. Es stellt aber auch für mit dem Bereich der Verifikation sequentieller Programme Vertraute ein gutes Hilfsmittel dar, sich in die besonderen Probleme paralleler und verteilter Programme einzuarbeiten. Die Beschränkung auf die grundlegenderen Konzepte paralleler und verteilter Programmierung verstärkt den Charakter einer Einführung. Das Buch kann vorlesungsbegleitend, aber auch zum Selbststudium eingesetzt werden.


Claus Pahl, Universität Dortmund, FB Informatik
pahl@ls10.informatik.uni-dortmund.de



zurück zur Startseite der Softwaretechnik-Trends , zu Band 15 Heft 1