Die Verifikation dient zum Test (kein Beweis) der Korrektheit von Programmen und wird in Verbindung eines Phasenmodells als Testphase bezeichnet.
Erst nachdem die Codierungsphase Implementation abgeschlossen ist und der vollständige Programmcode vorliegt, wird das Programm (hoffentlich) ausführlich getestet.
Es werden getestet:

• alle spezifizierten Methoden des gesamten Softwareprodukts und
• gegebenenfalls die konkreten Testfälle, die im Pflichtenheft stehen.

Die Verifikation ist kein Softwarebeweis, sondern ein Softwaretest.
Mit der Verifikation wird nicht bewiesen, dass ein Softwareprodukt korrekt ist. Es wird nur stichprobenartig geprüft, ob das Softwareprodukt erwartete Ausgaben liefert.

Trotz einer umfangreichen Testphase können jedoch immer noch Fehler unentdeckt bleiben.

• In [INFODUDEN S. 663] heißt es ganz treffend:
  „Durch Testen kann immer nur die Anwesenheit von Fehlern, nie jedoch deren Abwesenheit bewiesen werden.”
• Dijkstras Gesetz
  Viele Programmfehler treten nicht in der Testphase auf, sondern erst, wenn das Programm beim Kunden installiert ist (Vorführeffekt).

Programmfehler, die in dieser Phase nicht aufgedeckt und korrigiert werden können, müssen bei der Wartung behandelt werden und haben meist einen aufwändigen Rücksprung zur Implementation zur Folge.

Die Hauptpfade im System laufen meist zuverlässig. Fehler verbleiben meist in seltener durchlaufenen Pfaden.
Zur Korrektheit von Softwaresystemen stellte Dijkstra folgende Formel auf:

1. psys = pn
2. n ist die Anzahl der Komponenten im System.
3. p ist die Wahrscheinlichkeit, dass eine einzelne Komponente korrekt ist.
4. psys ist die Wahrscheinlichkeit, dass das gesamte System korrekt ist.

Betrachtet man diese Formel (wohl eher Faustregel), dann wird schnell klar, dass kein Softwaresystem korrekt sein kann.

Auch wenn das Softwareprodukt fertiggestellt, jedoch nicht ausführlich getestet, ist, sollte sich der Softwareproduzent nicht dazu verleiten lassen — sei es aus Zeitdruck oder auf Drängen des Kunden — es zum Einsatz freizugeben.
Der Softwareproduzent muss streng nach der Maxime handeln:

1. Vertrauen ist nichts, Kontrolle ist alles!

Fehler in den Hauptfunktionen können beispielsweise das gesamte Softwareprodukt unbrauchbar machen, und bei eher unbedeutenden Schönheitsfehlern verliert der Kunde das Vertrauen in das Produkt. In beiden Fällen zahlt der Softwareproduzent drauf. Deshalb muss das Softwareprodukt vollständig und ausgiebig auf Fehler geprüft werden, bevor es das Softwarehaus verlässt.

Erfahrungsgemäß kommt es während der Verifikation häufig zum aufwändigen Rücksprung in die Phase der Implementierung, wobei nach jedem Rücksprung die Verifikationsphase unglücklicherweise wieder von vorne anlaufen muss.
Da aber auch die Verifikation, also das Austesten eines bereits fertigen Produktes, wohl leicht auf der Strecke liegen bleiben kann, möchte man die Verifikation viel mehr vor die Phase der Implementierung ziehen.
Dabei stellt sich mit Recht die Grundsatzfrage, ob ein System schon getestet werden kann, ohne überhaupt den zu testenden Code zur Verfügung zu haben.

Wie soll das gehen? Ein Flugzeug kann beispielsweise erst getestet werden, nachdem es gebaut worden ist. Der Informatiker kann sich glücklicherweise im Sinne der Softwareproduktion weitgehend von Materie und Energie loslösen. Auf einer abstrakten Ebene gibt es praktisch kaum noch Grenzen.
Um die Korrektheit eines Softwareproduktes nachzuweisen, benötigt man streng genommen sowieso nur das Dokument der Spezifikationsphase, also das fertige, jedoch unimplementierte Softwareprodukt. Deshalb implementiert man zunächst alle erforderlichen Testfälle für jede einzelne spezifizierte Methode des Projekts, welche sich genau an die Spezifikationsbeschreibungen halten. Zudem sorgt man dafür, dass diese Testfälle wiederholbar sind und bzgl. anderer Testfälle isoliert ablaufen können, also jederzeit (voll automatisch) wiederholt werden können, ohne dabei eine Reihenfolge der Testfälle einhalten zu müssen. Jeder einzelne Testfall liefert ein Ergebnis — ob geglückt oder nicht. Wenn nun alle Testfälle des Projektes glücken, funktioniert die Projektsoftware korrekt gemäß der Spezifikation.
Da aber noch kein implementierter Code vorliegt, schlagen selbstverständlich zunächst alle Testfälle fehl. Erst mit der tatsächlichen Implementierung der Projektsoftware verringert sich die Anzahl der Fehlschläge nach und nach, bis schließlich keine mehr zu verzeichnen sind. Jede frisch implementierte Methode kann sofort und zu jeder anderen Zeit auf Korrektheit getestet werden.
Dieser Trend ist dem „Extreme Programming” sehr verwandt, mit dem Unterschied, dass hier alle Anforderungen bereits konkret vorliegen. Änderungen der Anforderungen sind hier zwar auch möglich, aber nicht zu erwarten. Das bedeutet, dass dieser Test nicht mehr geändert werden muss, wenn der Test der Methode einmal geschrieben ist.
Selbstverständlich ist die Korrektheit des endgültigen Softwareproduktes nach der Qualität der Testfälle zu beurteilen. Decken die Tests auch wirklich alle kritischen Fälle ab? Hierbei gilt der Grundsatz:

1. Immer auf der sicheren Seite bleiben!
   Lieber einen unbedeutenden Fall zu viel als einen notwendigen zu wenig!

Hierzu ein simples Szenario mit der Fakultätsfunktion faculty.

1. Spezifikation
   Als Erstes wird faculty spezifiziert.
2. Verifikation
   1. Nach der Spezifikation werden die Testfälle zu faculty implementiert.
   2. Die Testfälle zu faculty sollten in einem globalen Modultest integriert werden. Ein Modultest prüft alle testbaren Komponenten eines Moduls auf Korrektheit.
3. Implementation
   Erst im Anschluss der vorangegangenen Punkte wird faculty ausimplementiert, wobei faculty vor, während und nach (d. h. immer!) der Implementation getestet werden kann.

/* SPEZIFIKATION: faculty  *  * Die Fakultätsfunktion n! aus der Stochastik.  * Im Falle (-1 < n < 16) soll n! zurückgegeben werden,  * ansonsten -1.  */ long faculty(int n) {   /* ... hier fehlt noch die Implementation ... */   return 0; }

Jetzt „faculty” noch nicht ausimplementieren, auch wenn es so manchen in den Fingern kribbelt! :−(

/* VERIFIKATION: faculty  *  * Testet alle notwendigen Fälle der Fakultätsfunktion,  * gleichwohl ob bereits implementiert oder nicht.  *  * Dabei werden besonders die Grenzfälle betrachtet!  */ int testFaculty() {   if (faculty(-2) != -1) return 0;   else if (faculty(-1) != -1) return 0; // Grenzfall   else if (faculty(0) != 1) return 0; // Grenzfall   else if (faculty(1) != 1) return 0; // Grenzfall   else if (faculty(2) != 2) return 0;   else if (faculty(3) != 6) return 0;   else if (faculty(4) != 24) return 0;   else if (faculty(5) != 120) return 0;   else if (faculty(15) != 2004310016) return 0; // Grenzfall   else if (faculty(16) != -1) return 0; // Grenzfall   else if (faculty(17) != -1) return 0;   else return 1; // sonst kein Fehlschlag! }

Jetzt „faculty” noch nicht ausimplementieren, auch wenn das Kribbeln immer unerträglicher werden sollte, doch die Erlösung ist nah! :−)

void testMathModule() {   // ...   /* Testfälle zu faculty können jederzeit ausgeführt werden! */   if (testFaculty()) printf("faculty() okay!\n");   else printf("faculty() NOT okay!\n");   // ... }

Und endlich darf „faculty” ausimplementiert werden. :−)

/* IMPLEMENTATION: faculty  *  * Die Fakultätsfunktion n! aus der Stochastik.  * Im Falle (-1 < n < 16) soll n! zurückgegeben werden,  * ansonsten -1.  */ long faculty(int n) {   if (n < 0) return -1;   else if (n > 15) return -1;   else if (n == 0) return 1;   else return n * faculty(n - 1); }

Da die Funktion faculty() nun endlich ausimplementiert ist, kann sogleich der Mathematiktest mit der Funktion testMathModule() durchgeführt werden. Gegebenenfalls muss die Implementierung von faculty() nachkorrigiert werden.

Diese Vorgehensweise scheint jedoch recht umständlich zu sein, stellt sich aber bei konsequenter Einhaltung für jede Funktion bzw. Methode des Projektes als wahres Wundermittel heraus! Selbst bei der Wartung kann das bereits installierte Softwaresystem jederzeit erneut auf Korrektheit überprüft werden.
Auch wenn sich die Entwicklungszeit mit diesen zusätzlichen Testmethoden verlängert, wird es sich später an anderer Stelle bezahlt machen, denn

1. mit automatischen Tests wird letztendlich planmäßig entwickelt und nicht außerplanmäßig nach Fehlern gesucht.

Hat man nun eine stabil laufende Software entwickelt, fehlt meist noch die Optimierung. {Optimierungen haben in der Regel keinen Einfluss auf die bereits bestehenden Schnittstellen.} Optimiert man nun per Hand, entstehen meist grobe Fehler. Mit automatischen Tests deckt man schnell Fehler auf, die während der nachträglichen Optimierung entstanden sind.
Viele Java-Entwickler nutzen zur Verifikation das umfangreiche Package JUnit, womit sie automatische Tests (Unit−Tests) zum Softwareprodukt relativ schnell und komfortabel erstellen können. Mittlerweile gibt es schon fast zu jeder Sprache Testbibliotheken: .NET−Entwickler können zum Beispiel auf NUnit zurückgreifen und die Welt der Cpp-Programmierer kann nun auch nach dem Vorbild „JUnit” die Lib CppUnit verwenden. Die Verwendung von solchen Bibliotheken vereinheitlichen die Tests von Softwareprodukten und können — was noch viel wichtiger ist — als solides Verkaufsargument verwendet werden. Der Kunde ist schneller bereit, ein automatisch verifizierbares Softwareprodukt zu kaufen. {Zur Erinnerung: Ein automatisch verifizierbares Softwareprodukt ist nicht zwangsläufig frei von Fehlern! Für den Nachweis absoluter Korrektheit muss ein mathematischer, allumfassender Beweis existieren.}

Haben Sie beim Schach schon einmal mit dem Stickmatt …

… punkten können?

Mehr ...