Korrektheit

Man unterscheidet zwischen Prüfung der Korrektheit (Verifikation) und Prüfung der Spezifikation (Validierung). Ein Algorithmus heisst korrekt, wenn er sich gemäß seiner Spezifikation verhält, auch wenn seine Spezifikation nicht immer die gewünschten Ergebnisse liefert. Der Spezifikation beschreibt die Vorbedingungen (was vor der Anwendung des Algorithmus gilt, so dass der Algorithmus überhaupt angewendet werden darf) und die Nachbedingungen (was nach der Anwendung des Algorithmus gilt, welchen Zustand des Systems der Algorithmus also erzeugt). Hier geht es ausschliesslich um die Prüfung der Korrektheit eines Algorithmus, also darum, ob die spezifizierten Nachbedingungen wirklich gelten.

Nebenbemerkungen

es gibt Algorithmen, die nie mit einer 100-prozentigen Wahrscheinlichkeit richtige Ergebnisse liefern können (z.B. nichtdeterministische Primzahltests).
Korrektheit ist oft kein eigenständiges Kapitel in der Informatik, sondern wird meist unter dem Stichwort 'Softwaretest' geführt. Auch in Algorithmenbüchern wird Korrektheit meist nur im Zusammenhang mit konkreten Algorithmen behandelt, aber nicht als problemübergreifendes Konzept. Dies erscheint der Bedeutung von Korrektheit nicht angemessen.

Will man die Korrektheit eines Algorithmus/Programms feststellen, hat man 3 Vorgehensweisen zur Verfügung: Prüfung der syntaktischen Korrektheit, formaler Korrektheitsbeweis und Softwaretest.

Syntaktische Korrektheit

Die syntaktische Korrektheit behandeln wir hier nur kurz und der Vollständigkeit halber. Sie wird in den Veranstaltungen zur theoretischen Informatik (Grammatiken) und zum Compilerbau ausführlich behandelt.

Syntaktische Prüfung

Es wird eine Grammatik definiert, deren Regeln die Implementation des Algorithmus befolgen muss. Für ein Programm heisst das beispielsweise, dass die Syntax der Programmiersprache eingehalten werden muss.

Vorteile des Verfahrens: die Richtigkeit der Syntax lässt sich leicht vom Compiler/Interpreter überprüfen (mehr dazu in der Theoretischen Informatik und Compilerbau). Somit ist es die einfachste Möglichkeit, die Korrektheit zu überprüfen.

 >>> if a==0
   File "<stdin>", line 1
     if a==0
           ^
 SyntaxError: invalid syntax

Typprüfung

Ein Typ definiert Gruppierung der Daten und die Operationen, die für diese Datengruppierung erlaubt sind(konkreter Typ) bzw. die Bedeutung der Daten und die erlaubten Operationen (abstrakter Datentyp, vgl. Dreieck aus der ersten Vorlesung). Typen sind Zusicherungen an den Algorithmus und den Compiler/Interpreter, dass Daten und deren Operationen bestimmte semantische Bedingungen einhalten. Wenn man innerhalb des Algorithmus mit Typen arbeitet, darf man von der semantischen Korrektheit der erlaubten Operationen ausgehen. Umgekehrt können Operationen, die zu Typkonflikten führen würden, leicht als inkorrekt zurückweisen werden.

Vorteile des Verfahrens: Typprüfung ist teuerer als syntaktische Prüfung, aber billiger als andere Prüfungen der Korrektheit (mehr dazu im Kapitel Generizität).

 >>> a=3
 >>> b=None
 >>> a+b
 Traceback (most recent call last):
   File "<stdin>", line 1, in <module>
 TypeError: unsupported operand type(s) for +: 'int' and 'NoneType'

In python ist (ebenso wie in vielen anderen Programmiersprachen) explizite Typprüfung möglich:

 >>> import types
 >>> a=3
 >>> b=None
 >>> if isinstance(b, types.IntType): # prüft, ob b ein Integer ist
 ...     print a+b
 ... else:
 ...     raise TypeError, "b ist kein Integer" # falls b kein Integer ist, wird ein TypeError ausgelöst
 ... 

 Traceback (most recent call last):
   File "<stdin>", line 4, in <module>
 TypeError: b ist kein Integer

Formaler Korrektheitsbeweis

(Halb-)Automatisches Beweisen

Man versucht, die Hypothese H: Algorithmus ist korrekt entweder mathematische zu beweisen oder zu widerlegen. Dieses Beweisverfahren heisst dann halbautomatisch, wenn der Mensch in den Entscheidungsprozess miteinbezogen wird.

Um den Beweis durchführen zu können, ist folgendes nötig:

eine formale Spezifikation des Algorithmus: eine formale Spezifikation wird in einer Spezifikationssprache geschrieben (z.B. Z). Sie ist

deklarativ (d.h. beschreibt, was das Programm tun soll, ist selbst aber nicht ausführbar)
formal präzise (kann nur auf eine einzige Weise interpretiert werden)
hierarchisch aufgebaut (eine Spezifikation für einen komplizierten Algorithmus greift auf Spezifikationen für einfache Bestandteile dieses Algorithmus zurück)
so einfach, dass ihre Korrektheit für einen Menschen mit entsprechender Erfahrung unmittelbar einsichtig ist (denn eine Spezifikation kann nicht formal bewiesen werden - dafür wäre eine weitere Spezifikation nötig, die auch bewiesen werden müsste usw.)

ein axiomatisiertes Programmiermodell, z.B.

eine axiomatisierbare Programmiersprache, wie z.B. WHILE-Programm (s. erste Vorlesung), Pascal (siehe dazu Hoare's grundlegenden Artikel) und rein funktionale Programmiersprachen
ein axiomatisierbares Subset einer Programmiersprache (die meisten Programmiersprachen sind zu komplex, um als Ganzes axiomatisierbar zu sein)
endliche Automaten

Der Korrektheitsbeweis kann beispielsweise mit dem Hoare-Kalkül (Hoare-Logik) durchgeführt werden (Hoare erfand u.a. den Quicksort-Algorithmus). Diese Methode wurde in

C.A.R. Hoare: "An Axiomatic Basis for Computer Programming", Communications of the ACM 1969 [1]

erstmalig beschrieben. Im folgenden wird das Verfahren an einem Beispiel erläutert.

Beispiel-Algorithmus

Zuerst brauchen wir einen Algorithmus, den wir auf Korrektheit prüfen wollen. Wir nehmen als Beispiel die Division x/y durch sukzessives Substrahieren.

Vorbedingungen:
   int x,y
   x,y > 0
Gesucht:
   Quotient q, Rest r
Algorithmus:
   r = x
   q = 0
   while y <= r:
       r = r - y
       q = q + 1
Nachbedingungen:
   x == r + y*q and r < y

Aufbau der Hoare-Logik

Grundlegende syntaktische Struktur:

p {Q} r

mit p:Vorbedingung, Q: Operation, r: Nachbedingung. Es bedeutet also schlicht: wenn man im Zustand p ist und eine Operation Q ausführt, kommt man in den Zustand r. Hat eine Operation keine Vorbedingung, schreibt man

true {Q} r

Die Hoare-Logik besteht aus 5 Axiomen:

D0 - Axiom der Zuweisung

(Rule of Assignment)

R[t] {x=t} R[x]

Beispiel: t==5 {x=t} x==5

Vorbedingung und Nachbedingung sind gleich, mit Ausnahme der Variablen x und t, die in der Zuweisung verknüpft werden: Man erhält die Vorbedingung, wenn man in der Nachbedingung alle Vorkommen von x (bzw. allgemein alle Vorkommen der linken Variable der Zuweisung) durch t (bzw. durch die rechte Variable der Zuweisung) ersetzt.

D1 - Konsequenzregeln

(Rules of Consequence, besteht aus zwei Axiomen)

D1(a): wenn gilt

P {Q} R und R ⇒ S

dann gilt auch

P {Q} S

D1(b): wenn gilt

P {Q} R und S ⇒ P

dann gilt auch

S {Q} R

Beispiel: Für jede ganze Zahl gilt (x>5) ⇒ (x>0). Gilt außerdem (x>5) dann gilt erst recht (x>0).

D2 - Sequenzregel

(Rule of Composition)

wenn gilt

P {Q₁} R₁ und R₁ {Q₂} R

dann gilt auch

P {Q₁, Q₂} R

Das heisst: wenn man P hat und Q₁ darauf anwendet, kommt man zu R₁. Wenn man R₁ hat und Q₂ darauf anwendet, kommt man zu R. Deshalb kann man das so verkürzen: wenn man P hat und nacheinander Q₁ und Q₂ darauf anwendet, kommt man zu R.

D3 - Iterationsregel

(Rule of Iteration)

wenn gilt

(P ∧ B) {S} P

dann gilt auch

P { while B do S } (¬B ∧ P)

P wird dabei als Schleifeninvariante bezeichnet, weil es sowohl in der Vor- als auch in der Nachbedingung gilt. B ist die Schleifenbedingung - solange B erfüllt ist, wird die Schleife weiter ausgeführt.

Da wir in dem Divisions-Algorithmus mit dem Typ int arbeiten, brauchen wir außerdem die für diesen Typ erlaubten Operationen, also die Axiome der ganzen Zahlen.

A1: Kommutativität x+y=y+x, x*y=y*x

A2: Assoziativität (x+y)+z=x+(y+z), (x*y)*z=x*(y*z)

A3: Distributivität x*(y+z)=x*y+x*z

A4: Subtraktion (Inverses Element) y≤x ⇒ (x-y)+y=x

A5: Neutrale Elemente x+0=x, x*0=0, x*1=x

Beweisen des Algorithmus

Vorbedingung: 0 < y,x

Schleifeninvariante P (gleichzeitig Nachbedingung): x == y*q + r

 (1)  true ⇒ x==x+y*0                                          y*0==0 und x==x+0 folgen aus A5
 (2)  x==x+y*0              {r=x}                  x==r+y*0     D0: ersetze x durch r
 (3)  x==r+y*0              {q=0}                  x==r+y*q     D0: ersetze 0 durch q
 (4)  true                  {r=x}                  x==r+y*0     D1(b): kombiniere (1) und (2)
 (5)  true                  {r=x, q=0}             x==r+y*q     D2: kombiniere (4) und (3)
 (6)  x==r+y*q ∧ y=r ⇒ x==(r-y)+y*(1+q)                       folgt aus A1...A5
 (7)  x==(r-y)+y*(1+q)      {r=r-y}                x==r+y*(1+q) D0: ersetze (r-y) durch r
 (8)  x==r+y*(1+q)          {q=q+1}                x==r+y*q     D0: ersetze (q+1) durch q
 (9)  x==(r-y)+y*(1+q)      {r=r-y, q=q+1}         x==r+y*q     D2: kombiniere (7) und (8)
 (10) x==r+y*q ∧ y≤r       {r=r-y, q=q+1}         x==r+y*q     D1(b): kombiniere (6) und (9)
 (11) x==r+y*q    {while y≤r do (r=r-y, q=q+1)} x==r+y*q ∧ ¬(y≤r) D3: transformiere (10)
 (12) true        {while y≤r do (r=r-y, q=q+1)} x==r+y*q ∧ ¬(y≤r) D2: kombiniere (5) und (11)

Im obigen Beweis ergibt sich sogar true als Vorbedingung (i.e. es gibt keine Vorbedingung). Dies liegt daran, dass Hoare in seinem Artikel durchweg von nicht-negativen Zahlen ausgeht. Diese Annahme wird beim Beweis von Zeile (6) benutzt.

In der Praxis führt man solche Beweise natürlich nicht von Hand, sondern benutzt geeignete Programme, sogenannte automatische Beweiser, die man allerding oft interaktiv steuern muss, weil der Beweis ohne diese Hilfe zu lange dauern würde.

(Halb-)Automatisches Verfeinern

Dieses Verfahren ist beliebter, als das (Halb-)automatische Beweisen. Die formale Spezifikation wird nach bestimmten, Semantik-erhaltenden Transformationsregeln in ein ausführbares Programm umgewandelt. Mehr dazu z.B. in der Wikipedia (Program refinement). Der Vorteil dieser Methode besteht darin, dass man die Transformationsregeln so definieren kann, dass nur das axiomatisierte Subset der Zielsprache benutzt wird. Dadurch wird der Korrektheitsbeweis stark vereinfacht.

Software-Tests

Dijkstra [2] ließ einmal den Satz 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 sicherstellt, dass das Testprogramm einen vorhandenen Fehler zumindest mit hoher Wahrscheinlichkeit findet.

Ein Software-Test versucht, ein Gegenbeispiel zur Hypothese H "der Algorithmus ist korrekt" zu finden. Dabei gibt es 4 Möglichkeiten:

  Algorithmus	   Testantwort	
     +	               +	        Algorithmus ist richtig, kein Gegenbeispiel gefunden
     -	               -	        Alg. ist falsch, und der Test erkennt den Fehler
     +	               -	        Bug im Test (Gegenbeispiel, obwohl Alg. richtig ist)
     -	               +	        Test hat versagt, da er den Fehler im Alg. nicht erkannt hat

Wenn ein Gegenbeispiel zu H gefunden wird, kann man den Algorithmus (oder den Test) debuggen. Wird hingegen keines gefunden, nimmt man an, dass der Algorithmus korrekt ist. Man sieht, dass diese Annahme im Fall 4 nicht stimmt. Da Softwaretests jedoch in der Praxis sehr erfolgreich verwendet werden, ist dieser Fall offenbar nicht so häufig, dass man das Testen als Methode generell ablehnen müßte.

Freivalds-Algorithmus

Wir wollen die Wahrscheinlichkeit, dass ein Test einen vorhandenen Fehler übersieht, am Beispiel des Algorithmus von Freivalds studieren. Es handelt sich dabei um einen randomisierten Algorithmus zum Testen der Matrixmultiplikation (siehe J. Hromkovič: "Randomisierte Algorithmen", Teubner 2004). Ziel dieses Algorithmuses ist es, die Hypothese H "C ist das Produkt der Matreizen A und B" durch ein Gegenbeispiel zu widerlegen, ohne für den Test die Matrizenmultiplikation anzuwenden.

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

 (1) Initialisierung      
      wähle Zufallsvektor der Länge N aus Nullen und Einsen: <math>\alpha \in \{0, 1\}^N </math>  
 (2) Matrix-Vektor-Multiplikation (keine Matrix-Matrix-Multiplikation)

      <math>\left.\begin{array}{l}
               \beta = B*\alpha \\
               \gamma=A*\beta
               \end{array}\right\}A*(B*\alpha) == (A*B)*\alpha
      </math> 

      <math>\delta=C*\alpha</math>

 (3) Test der Korrektheit: falls A*B == C, liefert der folgende Test stets true:

      return   γ==δ

Wir analysieren nun, mit welcher Wahrscheinlichkeit der Algorithmus den Fehler findet, wenn es denn einen gibt, d.h.

Wahrscheinlichkeit p, dass Freivalds Algorithmus den Fehler findet

oder

Wahrscheinlichkeit q = 1 - p, dass Freivalds Algorithmus den Fehler nicht findet.

Wir schätzen diese Wahrscheinlichkeit ab für den einfachen Fall N=2. Wir definieren:

  <math>C=
 \begin{pmatrix} 
   c_{11} & c_{12}  \\ 
   c_{21} & c_{22}  
 \end{pmatrix},\qquad

\alpha=\begin{pmatrix}

   \alpha_1 \\
   \alpha_2 
    \end{pmatrix},\qquad
\delta=\begin{pmatrix}
   \delta_1 \\
   \delta_2
\end{pmatrix}
 = \begin{pmatrix}
   c_{11}\alpha_1 + c_{12}\alpha_2 \\
   c_{21}\alpha_1 + c_{22}\alpha_2
  \end{pmatrix}</math>

Fallunterscheidung:

Fall 1: C enthält genau 1 Fehler, z.B. <math>c_{11}</math> hat falschen Wert

Der Fehler wird gefunden, wenn <math>\delta_1 \ne \gamma_1 \Leftrightarrow\alpha_1\ne 0</math>. Da <math>\alpha_1</math> eine Zufallszahl aus <math>\{0,1\}</math> ist, folgt daraus, dass p = q = <math>\frac{1}{2}</math>

Fall 2: C enthält 2 Fehler

(a) in verschiedenen Zeilen und Spalten, z.B. <math>c_{11}</math> und <math>c_{22}</math>. Es gilt: Der Fehler in <math>c_{11}</math> wird gefunden, wenn <math>\delta_1 \ne \gamma_1 \Leftrightarrow \alpha_1\ne 0</math>. Unabhängig davon wird der Fehler in <math>c_{22}</math> gefunden, wenn <math>\delta_2 \ne \gamma_2 \Leftrightarrow \alpha_2\ne 0</math>. Da <math>\alpha_1</math> und <math>\alpha_2</math> statistisch unabhängig sind, ist die Wahrscheinlichkeit für jedes dieser Ereignisse <math>q_1</math> bzw. <math>q_2</math> jeweils <math>\frac{1}{2}</math>, und die Gesamtwahrscheinlichkeit q, dass keiner der beiden Fehler gefunden wird, ist deren Produkt: q = <math>q_1*q_2 = \frac{1}{2}* \frac{1}{2} = \frac{1}{4}</math>.

(b) in verschiedenen Zeilen, gleiche Spalten, z.B. <math>c_{11}</math> und <math>c_{21}</math>. Es gilt: Der Fehler in <math>c_{11}</math> wird gefunden, wenn <math>\delta_1 \ne \gamma_1 \Leftrightarrow \alpha_1\ne 0</math>. Das gleiche gilt für den Fehler in <math>c_{21}</math>. Die Wahrscheinlichkeit q, dass keiner der beiden Fehler gefunden wird, ist demzufolge: q = <math>\frac{1}{2}</math>.

(c) in der gleichen Zeile, z.B. <math>c_{11}</math> und <math>c_{12}</math>. Es gilt: Der Fehler wird gefunden, wenn <math>\delta_1 \ne \gamma_1 \Leftrightarrow \alpha_1*c_{11}+\alpha_2*c_{12}</math>. Hier treten nun zwei ungünstige Fälle auf:

1) Der Fehler wird u.a. dann nicht gefunden, wenn <math>\alpha_1 = \alpha_2=0</math>. Die Wahrscheinlichkeit dafür ist wieder q=<math>\frac{1}{4}</math>

2) <math>\alpha_1=\alpha_2=1</math> (dies geschieht ebenfalls mit Wahrscheinlichkeit <math>\frac{1}{4}</math>), aber die Werte <math>c_{11}</math> und <math>c_{12}</math> sind "zufälligerweise" so falsch, dass sich die Fehler gegenseitig aufheben. Die Wahrscheinlichkeit, dass beide Bedingungen gelten, ist auf jeden Fall q = <math>\epsilon<\frac{1}{2}</math>.

Analog behandelt man die Fälle, dass C drei oder vier Fehler enthält. Fasst man die Fälle zusammen, ergibt sich, dass die Wahrscheinlichkeit, einen vorhandenen Fehler nicht zu entdecken, sicher kleiner als <math>\frac{1}{2}</math> ist. Dies gilt auch allgemein:

Satz

Die Wahrscheinlichkeit, dass Freivalds Algorithmus einen vorhandenen Fehler nicht findet, ist q < <math>\frac{1}{2}</math>

Folgerung

Lässt man Freivalds Algorithmus mit verschiedenen <math>\alpha</math> k-mal laufen, gilt <math>q_k < 2^{-k}</math> für die Wahrscheinlichkeit, dass keiner der k Durchläufe einen vorhandenen Fehler findet. Diese Wahrscheinlichkeit konvergiert sehr schnell gegen 0. Das heisst, der Algorithmus findet mit beliebig hoher Wahrscheinlichkeit ein Gegenbeispiel zu H (falls es eins gibt), wenn man ihn nur genügend oft mit jeweils anderen Zufallszahlen wiederholt. Daraus folgt, dass Testen ein effektives Fehlersuchverfahren sein kann -- die oben erwähnten Einschränkung von Dijktra trifft zwar zu, aber Tests, die mit so hoher Wahrscheinlichkeit funktionieren, sind für die Praxis vollkommen akzeptabel.

Vergleich formaler Korrektheitsbeweis und Testen

Nachdem nun die formalen Methoden sowie der Software-Test vorgesellt worden sind, ist nun die Frage, welcher der beiden Vorgänge der bessere ist, aufzugreifen. Allgemein gilt:

randomisierte Algorithmen

sind schnell und einfach:

da die Operationen einfach sind und wenig Zeit kosten
des öfteren eine Auswahl vorgenommen wird ohne die Gesamtmenge näher zu betrachten
die Auswahl selbst aufgrund einfacher Kriterien (bspw. zufällige Auswahl) erfolgt

können Lösungen approximieren und liefern gute approximative Lösungen

formaler Korrektheitsbeweis mit deterministischen Algorithmen (siehe auch [3])

bei jedem Aufruf des Beweisers werden immer die selben Schritte durchlaufen
keine Zufallswerte
komplexer Aufbau
oft sehr lange Laufzeit, z.B. mehrere Tage oder gar Monate

Für die formalen Methoden spricht, dass man mit ihnen im Prinzip beweisen kann, dass H nun entweder tatsächlich falsch oder richtig ist. Die formalen Beweise bei realen Problemen sind allerdings so kompliziert, dass sie ebenfalls mit Computerhilfe erbracht werden müssen. Dadurch liegt auch hier keine 100%-ige Korrektheitsgarantie vor: Auch formale Methoden können zum falschen Ergebnis kommen, z.B. durch Hardwarefehler, Compilerbugs, oder unvorhergesehenen Bitumfall (diese Gefahr ist z.B. im Weltall wegen der kosmischen Strahlung deutlich größer). Die Möglichkeit von Hardwarefehlern wirkt sich auf die formalen Methoden wesentlich stärker aus, weil diese typischerweise wesentlich längere Laufzeiten haben als entsprechende Testalgorithmen. Es kann deshalb durchaus vorkommen, dass Tests eine höhere Erfolgswahrscheinlichkeit haben als ein formalen Beweis, wie die folgende Rechnung zeigt. Wir nehmen an, dass die Hardware eine "Halbwertszeit" von 50 Millionen Sekunden hat, d.h. ein Hardwarefehler tritt im Durchschnitt etwa alle 20 Monate auf. Dann ist die Wahrscheinlichkeit, dass ein deterministischer Algorithmus nicht zum Ergebnis (oder zum falschen Ergebnis) kommt:

<math>q_{\mathrm{Beweis}} \approx 0.001</math>, falls der Beweisalgorithmus 1 Tag benötigt,
<math>q_{\mathrm{Beweis}} \approx 0.01</math>, falls der Beweisalgorithmus 1 Woche benötigt,
<math>q_{\mathrm{Beweis}} \approx 0.035</math>, falls der Beweisalgorithmus 1 Monat benötigt.

Zum Vergleich nehmen wir an, dass der entsprechende Softwaretest einmal pro Sekunde ausgeführt werden kann, und dass jeder Durchlauf den Fehler mit einer Wahrscheinlichkeit von <math>\frac{1}{2}</math> nicht findet. Unter gleichzeitiger Berücksichtigung der Wahrscheinlichkeit von Hardwarefehlern gilt dann

<math>q_{\mathrm{Test}} \approx 0.5</math>, falls der Test 1 mal wiederholt wird,
<math>q_{\mathrm{Test}} \approx 0.001</math>, falls der Test 10 mal wiederholt wird,
<math>q_{\mathrm{Test}} \approx 10^{-6}</math>, falls der Test 100 mal wiederholt wird.

Mit anderen Worten: hier ist das Testen vorzuziehen, weil es unter realistischen Bedingungen eine höhere Erfolgswahrscheinlichkeit hat als der formale Beweis. Leider gibt es bisher keine Theorie, mit deren Hilfe man für ein gegebenes Problem systematisch Tests konstruieren kann, deren Misserfolgswahrscheinlichkeit bei wiederholter Anwendung garantiert so schnell gegen Null konvergiert wie die des Freivalds Algorithmus. Dies ist ein offenes Problem der Informatik.

Anwendung des Softwaretestverfahren

Beispiel an Python-Code

Man betrachte die Aufgabe, aus einer Zahl x die Wurzel zu ziehen. Dies kann man erreichen, indem man mit Hilfe des Newtonschen Iterationsverfahrens eine Nullstelle des Polynoms

sucht. Ist eine Näherungslösung <math>y^{(t)}</math> bekannt, erhält man eine bessere Näherung durch

<math>y^{(t+1)} = y^{(t)} - \frac{f(y^{(t)})}{f'(y^{(t)})}</math>.

Mit <math>f'(y) = -2y</math> wird das zu

<math>y^{(t+1)} = y^{(t)} + \frac{x-(y^{(t)})^2}{2y^{(t)}}=\frac{y^{(t)}+x/y^{(t)}}{2}</math>.

Dies kann man durch das folgende (allerding noch nicht korrekte) Pythonprogramm realisieren:

          1   def sqrt(x):
          2       if (x<0):
          3           raise DomainError("sqrt of negative number")
          4       y = x / 2
          5       while y*y != x:
          6           y =(y + x/y) / 2
          7      return y:

[um für den oben aufgeführten Pythoncode einen Test zu erstellen/ schreiben <math>\rightarrow</math> Unit-Test heranziehen (Übungsaufgabe)]

Es gilt nun den Pythoncode genauer zu betrachten:

Vorerst dienen folgende Testfunktionen als Orientierung

def testsqrt (self) : man muss prüfen, ob man bei einer negativen Zahl x eine Exception ausgelöst wird; dafür benötigt man assertRaises(Domain Error, sqrt,-1) <math>\Rightarrow</math> sollte hier keine Exception ausgelöst werden, dann würde der Test hier einen Fehler signalisieren
assertEqual(sqrt(9),3) <math>\Rightarrow</math> ist hier nicht 3 das Ergebnis, ebenfalls Fehlersignalisierung
assertEqual(sqrt(1),1)

und zum Zweiten, zwei wichtige Prinizipien, die wir anschließend auf den Pseudo-Code zur Verbesserung anwenden:

measure used in software testing

Prinzip der Domain Partitioning[4]

hier wird die einzusetzende Zahl ausgewählt
man teilt die Werte, die sich im Algorithmus gleich verhalten, in Wertebereiche ein:

<math>\Rightarrow</math> 1) wähle aus jedem Intervall min einen repräsentativen Wert

<math>\Rightarrow</math> 2) wähle aus jedem Intervall die Randwerte (diese sind interessant, da die meisten Programmierfehler am Rand der Schleife passieren, z.B. Indexfehler oder die "0" wird falsch behandelt)

Prinzip Code Coverage[5]

statement coverage : jedes Statement wird durch min. einen Test ausgeführt
condition coverage : jede if. Abfrage sollte min. einmal mit true und einmal mit false durchlaufen werden
path coverage : jeder Pfad wird einmal durchlaufen [in der Praxis wird allerdings nur eine Näherung erreicht)

Anwendung der Prinzipien auf den Pseudo- Code

Den ersten Bug findet man, wenn man versucht Zeile 5 anzuwenden. Bei einer Integer-Division wird nämlich abgerundet und 3 wird nicht als Endergebnis ausgegeben <math>\Rightarrow</math> Befehl einbauen, der in reelle Zahlen umwandelt.Desweiteren ist hier noch zu beachten, dass durch das einfügen eines float-Befehls Zeile 5 zu einer Endlosschleife wird, da keine Gewissheit mehr gegeben ist, dass tatsächlich beides gleich ist Punkt 2) vom Prinzip der Domain Partitioning zeigt den zweiten Bug an <math>\Rightarrow</math> Behandlung der "0" Der dritte Bug befindet sich in Zeile 4, nämlich, dass man bei Division durch "0" eine Errorfehlermeldung erhalten würde.

<math>\Rightarrow</math> verbesserter Code

‎

die ergänzenden Testfunktionen

assertRaise (DomainError,sqrt,-1)

assertEqual(sqrt(1),1)

asserAlmostEqual (sqrt(0),0,14)[grün]

asserAlmostEqual(sqrt(9),3,14) <math>\rightarrow</math> Dezimalplaces[blau]

assertEqual(sqrt(4),2) condition caverage

Korrektheit

Contents

Syntaktische Korrektheit

Syntaktische Prüfung

Typprüfung

Formaler Korrektheitsbeweis

(Halb-)Automatisches Beweisen

Beispiel-Algorithmus

Aufbau der Hoare-Logik

Beweisen des Algorithmus

(Halb-)Automatisches Verfeinern

Software-Tests

Freivalds-Algorithmus

Vergleich formaler Korrektheitsbeweis und Testen

Anwendung des Softwaretestverfahren

Beispiel an Python-Code

measure used in software testing

Anwendung der Prinzipien auf den Pseudo- Code

Navigation menu

Page actions

Page actions

Personal tools

Navigation

Search

Tools