\documentstyle[twocolumn,german]{article}
\input{trendsstyle.tex}

\begin{document}
\thispagestyle{empty}
\baselineskip11.64pt


\twocolumn[{\vspace*{-5mm}
\huge\sf Buchbesprechungen
\\[4mm]
}]

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

\noindent
{\bf CR-Klassifikation}: D.1.3-4, D.2.4, D.3.1, D.4.1, 
\\ \hbox{F.3.1-3}\\
{\bf Schl"usselw"orter}: Programmverifikation,
deterministische / nichtdeterministische sequentielle
Program\-me, parallele Programme, verteilte Programme


\medskip\noindent Das Buch bietet eine {\sl Einf"uhrung}
in die Problematik der {\sl Programmverifikation}.  Der
Schwerpunkt liegt auf der Darstellung m"oglicher
Fehlersituationen, die bei der Entwicklung verschiedener
Programmklassen entstehen k"onnen, 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 "Uber"-setzung ist
gegen"uber der englischen Originalfassung von 1991 um die
Aspekte Fairne"s und verteilte Terminierung gek"urzt und
umfa"st nun vom Umfang den Stoffinhalt einer vierst"undigen
einsemestrigen Vorlesung.

{\sl Korrektheit} ist ein bedeutender Qualit"atsfaktor bei
der Entwicklung von Programmen.  Das Buch beginnt mit
einer Veranschaulichung von m"oglichen Fehlersituationen
und Ma"snahmen zur Sicherung der Korrektheit an einem
Beispiel.  Die zum Verst"andnis von Programmiersprachen
und Logik notwendigen Grundlagen werden in knapper Form
angegeben.  Die Semantik der Programme wird mit Hilfe der
f"ur pa"-rallele oder verteilte Programme "ublichen
strukturell operationalen Semantik definiert.  Begriffe
wie Interpretation einer Spezifikationslogik und
Grundelemente von Beweissyste\-men werden kurz eingef"uhrt.
In den folgenden Abschnitten werden Verifikationstechniken
f"ur {\sl verschiedene Programmklassen} behandelt.  Zu
diesen geh"oren {\sl deterministische sequentielle,
disjunkte pa"-rallele, parallele mit gemeinsamen Variablen,
parallele mit Synchronisation, nichtdeterministische} und
{\sl verteilte Programme}.  Der Schwerpunkt dieses Buches
liegt auf den parallelen und verteilten Programmen.  Daher
werden diese auch schrittweise in mehreren Programmklassen
eingef"uhrt, die dem gegen"uber sequentiellen Programmen
erschwerten Verst"andnis solcher Programme Rechnung
tragen.  Die sequentiellen Programme werden nur soweit
betrachtet, wie sie f"ur das Verst"andnis weiterer
Sprachklassen notwendig sind.  Jedes Kapitel, das eine
Programmklasse beschreibt, umfa"st eine {\sl informelle
und formale Definition} der Sprachklasse, ein {\sl
Beweissystem}, eine oder mehrere {\sl Fallstudien}, sowie
{\sl "Ubungs"-aufgaben} und {\sl bibliographische Hinweise}.
F"ur jede Programmklasse werden Beweissyste\-me zur
partiellen und totalen Korrektheit des
Ein-/Ausgabeverhaltens angegeben; f"ur parallele und
verteilte Programme wird der Begriff der schwachen totalen
Korrektheit eingef"uhrt.  Konsistenz und f"ur eine
Programmklasse exemplarisch auch Vollst"andigkeit dieser
Beweissysteme werden gezeigt.  Die Fallstudien behandeln
"ubliche Problemstellungen aus den jeweiligen
Programmklassen, wie den wechselseitigen Ausschlu"s oder
das Erzeuger/Verbraucher-Problem.  Es werden zudem Aspekte
wie die systematische Programmentwicklung nach Dijkstra
und Gries oder Programmtransformation behandelt.  F"ur die
gestellten Aufgaben werden keine L"osungen angeboten.  Der
Anhang fa"st Programmsemantiken, Beweissyste\-me und
Beweisskizzen zusammen.

Die bibliographischen Hinweise sind gegen"uber der
Originalversion des Buches aktualisiert und bieten somit
einen guten "Uber\-blick "uber alle weitergehenden Aspekte
der Programmverifikation bis hin zu aktuellsten
Entwicklungen.  In den bibliographischen Hinweisen werden
auch alternative Ans"atze beleuchtet.  Etwa wird die
Synchronisation paralleler Programme "uber das
$await$-Konstrukt nach Owicki und Gries definiert. Vor-
und Nachteile gegen"uber 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"ucher, wie das
1989 bei Hanser in deutscher "Uber"-setzung erschienene {\em
Programmkonstruktion und Verifikation} von R. Backhouse,
{\em Programmentwicklung und Verifikation} von G. Futschek
(ebenfalls 1989 bei Springer erschienen) oder {\em
Einf"uhrung in die Programmverifikation} von B. Hohlfeld
und W. Struckmann (1992 im BI-Wis"-senschaftsverlag
erschienen), legen ihren Schwerpunkt auf die Betrachtung
deterministischer, sequentieller Programme.  Im
englischsprachigen Bereich ist das Buch in bezug auf die
inhaltliche Ausrichtung mit {\em 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"uh\-rung 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"azise dargestellt.  Das Buch richtet sich zwar in
erster Linie an Einsteiger in den Bereich Verifikation,
und setzt au"ser einem grundlegenden Verst"andnis von
Programmiersprachen und mathematischem Grundwissen keine
konkreten Kenntnisse voraus.  Es stellt aber auch f"ur mit
dem Bereich der Verifikation sequentieller Programme
Vertraute ein gutes Hilfsmittel dar, sich in die
besonderen Probleme paralleler und verteilter Programme
einzuarbeiten.  Die Beschr"ankung auf die grundlegenderen
Konzepte paralleler und verteilter Programmierung
verst"arkt den Charakter einer Einf"uhrung.  Das Buch kann
vorlesungsbegleitend, aber auch zum Selbststudium
eingesetzt werden.

\medskip
\noindent
Claus Pahl,  Universit"at Dortmund, FB Informatik\\
pahl@ls10.informatik.uni-dortmund.de

\end{document}

