7.2 Invarianten als Codeinstrumentierungen

Einer der Nachteile einer Testfallmodellierung im Stil der Abbildung 6.7 ist die fehlende Möglichkeit, während des Testablaufs Invarianten zu prüfen. Wird zum Beispiel ein komplexer Algorithmus bearbeitet, so kann es sinnvoll sein, statt nur das Ergebnis zu prüfen und damit auf interne Zwischenzustände rückschließen zu müssen, direkt die zwischendurch geltenden Eigenschaften zu formulieren und zu prüfen. Zu diesem Zweck wurde in Anhang B, Band 1 die bereits mehrfach genutzte ocl-Anweisung mit einer OCL-Bedingung als zu prüfende Zusicherung eingeführt. Ergänzt wird diese durch eine let-Anweisung zur Definition lokaler Variablen, die in späteren OCL-Invarianten verwendet werden können, um damit auf frühere Zustände zurückzugreifen.¹

Das Beispiel in Abbildung 7.4 demonstriert die Verwendung von ocl- und let-Anweisungen anhand einer Methode der Klasse Auction zur Versendung von Nachrichten.

Java/P        class Auction {

addMessage(Message m) {

ocl !this.message.contains(m);

let oldMessageSize = message.size;

message.add(m);

ocl message.size == oldMessageSize +1;

for(Iterator<Person> ip = bidder.iterator();

ip.hasNext(); ) {

Person p = ip.next();

p.addMessage(m);

ocl MessagesDelivered(this,p);

}

}}

Abbildung 7.4: Zusicherungen als ocl-Anweisungen

Eine ocl-Anweisung ist, wie in Abbildung 7.4 gezeigt, mit einer OCL-Bedingung oder einer Referenz auf eine benannte OCL-Invariante versehen. Im Beispiel wurde auf die folgende OCL-Invariante Bezug genommen, die eine allgemeine Beziehung zwischen einer Auktion und der eine Nachricht empfangenden Person beschreibt:

OCL       import Auction a, Person p inv MessagesDelivered:

Da Objektdiagramme sich nach Abschnitt 4.4, Band 1 hervorragend als prädikative Beschreibung eines Zustands eignen, lassen sich damit natürlich auch Objektdiagramme sowie die in Abschnitt 4.3, Band 1 diskutierte Kombination von Objektdiagrammen und der OCL als Zusicherungen einsetzen.

Es ist auch möglich, lokale Variablen innerhalb von Schleifen zu definieren. Die mit let eingeführten Variablen sind zwar unveränderbar, haben aber denselben Sichtbarkeitsbereich wie normale lokale Java-Variablen und werden daher bei jedem Schleifendurchlauf neu belegt. So lässt sich zum Beispiel die Terminierung der in Abbildung 7.5 gegebenen (nicht ganz trivialen) Schleife prüfen.

Java/P          int n = ...;

while( n>0 ) {

let nOld = n;

if( n % 1 == 0 ) n = n/2; else n = n-1;

// Verwendung von n …

ocl nOld > n;     // absteigende Werte

ocl nOld > 0;     // Begrenzung durch 0

}

ocl n<=0;           // Nach der Schleife gilt

Abbildung 7.5: Zusicherungen, die die Terminierung zeigen

Zur Terminierung der Schleife in Abbildung 7.5 wird die stetig absteigende und nach unten durch 0 begrenzte Variable n verwendet, deren alter Wert in nOld zwischengespeichert wird.

Die Erweiterung von Java um die beiden Anweisungen ist relativ stark angelehnt an die Zusicherungslogik, die sich derselben Techniken bedient, um Aussagen über Programme zu beweisen. Tatsächlich können die beschriebenen Hilfsmittel weit mehr als nur exemplarische Tests unterstützen. Ein geeigneter Beweiskalkül für Java, wie er zum Beispiel in [vO01, RWH01] diskutiert wird, kann damit verifizieren, dass Invarianten immer gelten. Allerdings ist in einem objektorientierten System die Entwicklung einer ausreichend vollständigen Menge von Zusicherungen im Code, so dass ein Verifikationswerkzeug die Korrektheit prüfen kann, sehr aufwändig. Ein solches Vorgehen kann aber vor allem für spezifische Aufgabenstellungen, wie komplexe Algorithmen, Protokolle oder Kernelemente der Sicherheitsarchitektur von Interesse sein.

Die Instrumentierung des Produktionscodes mit Prüfungen für Invarianten muss vom Compiler flexibel gehandhabt werden können. Im laufenden Betrieb sollte die Instrumentierung unterbleiben, im Probebetrieb eine für den Anwender unsichtbare Instrumentierung mit Ausgabe im Hintergrund (Protokoll) möglich sein und im Testsystem eine für Testfälle geeignete Instrumentierung durch Ausgabe und Fehleranzeige mittels JUnit erfolgen.

Bernhard Rumpe. Agile Modellierung mit UML. Springer 2012