Korrektheit

24.April ( erst nur ein formales Skelett, Feinarbeit folgt noch)

Ergänzend zum Beispiel der Hoare-Logic, die benutzt wurde um praxisorientiert mit der formale Methoden zu arbeiten, ein kurzer Verweis auf die benutzte Quelle : " An Axiomatic Basis for Computer Programming" , C.A.R. Hoave; Comm ACM 1969[1]

Software- Test

Dijkstra [2]ließ eimal das Zitat verlauten : " Tests können nie die Abwesenheit von Fehlern beweisen [Anwesenheit schon]"

Nach solch einer Aussage stellt sich die Frage ob es sich überhaupt lohnt, mit dem Testverfahren die Korrektheit eines Algorithmus zu zeigen. Es erscheint einem doch plausibler sich auf die "formalen Methoden" zu berufen , mit dem Wissen, dass diese uns tatsächlich einen Beweis liefern können ob nun H oder nicht H gilt. Zudem kommt noch erschwerend hinzu, dass es bei Tests bisher keine Theorie gibt, die mit hoher Wahrscheinlichkeit einen Fehler im Testprogramm findet.

Wie arbeitet nun ein Software-Test[3]? Grob beschrieben gibt es 4 Möglichkeiten: entweder man findet ein Gegenbeispiel zu H oder aber keines, das heißt H ist richtig. Falls keines von Beiden zutrifft, bestehen die zwei übrigen Methoden darin zu debuggen.

  Algorithmus	   Testantwort	
     +	               +	        Algorithmus ist richtig
     -	               -	        Alg. Ist zwar falsch, dennoch erkennt der Test den Fehler
     +	               -	        Bug im Test
     -	               +	        Test hat versagt, da er den Fehler im Alg. nicht erkannt hat

Softwaretests allerdings werden heutzutage oft durchgeführt, z.b. PC-Spiele, weshalb eine große Motivation vorliegt, sich sein Verfahren einmal genauer an dem "Fraivaldsalgorithmus" von Hrmkowic anzuschauen bzw durchzuführen.

gegeben:

        Matrizen A, B, C  der Größe NxN 
        H:  C=A*B  Matrixmultiplikation

1 wähle Zufallsvektor <math>alpha</math><math>element</math>{0,1}^N