Übersicht Inhaltsverzeichnis Vorwort 1 Einführung 2 Agile und UML-basierte Methodik 3 Kompakte Übersicht zur UML/P 4 Prinzipien der Codegenerierung 5 Transformationen für die Codegenerierung 6 Grundlagen des Testens 7 Modellbasierte Tests 7.1 Testdaten und Sollergebnis mit Objektdiagrammen 7.2 Invarianten als Codeinstrumentierungen 7.3 Methodenspezifikationen 7.4 Sequenzdiagramme 7.5 Statecharts 7.6 Zusammenfassung und offene Punkte beim Testen 8 Testmuster im Einsatz 9 Refactoring als Modelltransformation 10 Refactoring von Modellen 11 Zusammenfassung und Ausblick Literatur |
7.2 Invarianten als CodeinstrumentierungenEiner 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.1 Das Beispiel in Abbildung 7.4 demonstriert die Verwendung von ocl- und let-Anweisungen anhand einer Methode der Klasse Auction zur Versendung von Nachrichten.
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:
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.
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.
|
||||||||||||||||||||||||||||||||||||