7.5 Spezifikation, Entwurf und Verifikation mit Kastenstrukturen

Eine Methode, die für Cleanroom typisch ist und die formale Spezifikation mit der schrittweisen Verfeinerung verbindet, ist die Spezifikation und der Entwurf mit Kastenstrukturen (box structures). Dabei gibt es drei Sichten auf eine Softwarekomponente: Die reine Spezifikation (black box view), die Zustandsbeschreibung (state box view) und die Prozeßbeschreibung (clear box view). Die Bezeichnung Kastenstruktur weist darauf hin, daß jede dieser Beschreibungen in sich abgeschlossen ist.

7.5.1 black box, state box, clear box

Die black box view beschreibt die Reaktionen der Komponente ausschließlich über Eingabehistorien. Sie ist völlig implementationsunabhängig und betrachtet die Softwarekomponente als mathematische Funktion.

Die state box view stellt demgegenüber zumindest einen Teil der Eingabehistorien durch innere Zustände der Komponente dar und modelliert die Ausgaben als Reaktion auf momentane Eingaben und Zustände. Dies ist der erste Schritt auf dem Weg zu einer Implementation.

Die clear box view komplettiert einen Verfeinerungsschritt im Entwurf, indem die Ausgaben beschrieben werden über gegenwärtige Eingaben, Zustände und die Benutzung von black box views der Teilkomponenten niedrigerer Verfeinerungsstufen.

Für verschiedene Aspekte des Softwareentwurfs haben die datenorientierte Zustandsbeschreibung oder die vorgangsorientierte Prozeßbeschreibung Vorteile gegenüber der jeweils anderen. Es ist deshalb günstig, daß in dieser Vorgehensweise beide Methoden vereint werden.

Ein Verfeinerungsschritt geht also in folgenden Teilschritten vor sich:

• Definiere die black box:
  (1) Definiere Eingaben,
  (2) Definiere Ausgaben anhand der Eingabehistorien.
• Definiere die state box:
  (3) Definiere Zustände zur Repräsentation der Eingabehistorien,
  (4) Wähle Zustandsdaten aus, die auf dieser Ebene verwaltet werden sollen,
  (5) Formuliere black box neu, so daß sie die Ausgaben anhand von Eingaben und Zustandsdaten dieser Ebene beschreibt,
  (6) Verifiziere die state box.
• Definiere die clear box:
  (7) Definiere Datenabstraktion für die Zustandsdaten,
  (8) Formuliere state box neu, so daß sie die Ausgaben anhand von Eingaben, Zustandsdaten dieser Ebene und Aufrufen von black boxes noch zu definierender niederer Ebenen beschreibt,
  (9) Verifiziere die clear box.

Weitere Verfeinerungsschritte beginnen dann mit den black boxes, die in der clear box eingeführt wurden, es sei denn, diese werden als elementar betrachtet und nicht weiter verfeinert.

7.5.2 Beispiel

Das folgende Beispiel soll einen groben Eindruck davon vermitteln, wie diese fortgesetzte Verfeinerung vor sich geht und wie sie mit der Verifikation zusammenspielt. Das Beispiel ist natürlich ein reines Spielzeugbeispiel. In einer wirklichen Anwendung von Cleanroom wären die einzelnen Verfeinerungschritte umfangreicher und der Anwendungsfall auch komplizierter. Das Beispiel verzichtet auch völlig auf eine state box, weil es sich nur um ein Prädikat handelt, zu dessen Realisierung kein Zustand nötig ist.

$\bullet$black box 1: dreieckstyp (a,b,c)
Vorbedingung: a, b, c sind positive reelle Zahlen
Nachbedingung: Liefert GLEICHSEITIG bzw. GLEICHSCHENKLIG bzw. SONSTIGES bzw. KEINDREIECK, wenn das Tripel (a,b,c)Seitenlängen eines gleichseitigen bzw. nichtgleichseitigen gleichschenkligen bzw. eines nichtgleichschenkligen Dreiecks bezeichnet bzw. überhaupt nicht ein Tripel von Seitenlängen eines Dreiecks sein kann.

$\circ$clear box 1: dreieckstyp (a,b,c)
IF alle seiten erfüllen dreiecksungleichung (a,b,c)
THEN Liefere echter dreieckstyp (a,b,c)
ELSE Liefere KEINDREIECK

$\bullet$black box 2: alle seiten erfüllen dreiecksungleichung (a,b,c)
Vorbedingung: a, b, c sind positive reelle Zahlen.
Nachbedingung: True, falls jede Seite kürzer als die Summe der beiden anderen; False andernfalls.

$\bullet$black box 3: echter dreieckstyp (a,b,c)
Vorbedingung: (a, b, c) sind die Seitenlängen eines echten Dreiecks
Nachbedingung: Liefert GLEICHSEITIG bzw. GLEICHSCHENKLIG bzw. SONSTIGES, wenn das Tripel (a,b,c) die Seitenlängen eines gleichseitigen bzw. nichtgleichseitigen gleichschenkligen bzw. eines nichtgleichschenkligen Dreiecks bezeichnet.

$\star$Verifikation clear box 1:
Die drei Seiten können genau dann ein Dreieck bilden, wenn die beiden kürzeren, sagen wir x und y, zusammen länger sind als die längste, z. Dann nämlich können sie einen Winkel bilden, dessen Enden von einem Ende von z zum anderen reicht. z < x+y (also: ,,Dreiecksungleichung gilt für die Seite z``) ist also hinreichend, damit ein Dreieck vorliegt. Außerdem ist die Geltung der Dreiecksungleichung notwendig für jede Seite, damit ein Dreieck vorliegt. z < x+y gilt insbesondere, falls die Dreiecksungleichung für jede Seite gilt.
Damit liefert alle seiten erfüllen dreiecksungleichung die Aussage, daß es sich wirklich um ein Dreieck handelt, die Vorbedingung von echter dreieckstyp wird erfüllt, und clear box 1 ist korrekt.

Ende von Verfeinerungsschritt 1.

$\circ$clear box 2: alle seiten erfüllen dreiecksungleichung (a,b,c)
Liefere (a < b+c AND b < a+c AND c < a+b)

$\star$Verifikation clear box 2:
3 verschiedene, korrekte Fälle geprüft, UND-verknüpft; ist offensichtlich korrekt.

Ende von Verfeinerungsschritt 2.

$\circ$clear box 3: echter dreieckstyp (a,b,c)
IF a = b = cTHEN Liefere GLEICHSEITIG ELSE IF a = b OR a = c OR b = cTHEN Liefere GLEICHSCHENKLIG ELSE Liefere SONSTIGES

$\star$Verifikation clear box 3:
SONSTIGES ist als NOT gleichschenklig korrekt geprüft laut black box 1.
gleichseitig ist ein Spezialfall von gleichschenklig und muß deshalb zuerst geprüft werden, dies geschieht hier.
Deshalb ist clear box 3 korrekt.

Ende von Verfeinerungsschritt 3.