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 {Q1} R1 und R1 {Q2} R
- dann gilt auch
- P {Q1, Q2} R
- Das heisst: wenn man P hat und Q1 darauf anwendet, kommt man zu R1. Wenn man R1 hat und Q2 darauf anwendet, kommt man zu R. Deshalb kann man das so verkürzen: wenn man P hat und nacheinander Q1 und Q2 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.
Beispiel für das Testen: 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 Matrizen A und B" durch ein Gegenbeispiel zu widerlegen, wobei der Test einen anderen Algorithmus verwendet, um vergleichsdaten zu gewinnen.
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, denn die soll ja gerade verifiziert werden)
<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, gleichen 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}\ne 0</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
- <math>f(y) = x - y^2 = 0</math>
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>.
Im Spezialfall des Wurzelziehens war diese Newtoniteration übrigens bereits wesentlich früher als Babylonische Methode bekannt. Man kann diesselbe durch das folgende (allerding noch nicht korrekte) Pythonprogramm realisieren:
1 def sqrt(x):
2 if (x<0):
3 raise ValueError("sqrt of negative number")
4 y = x / 2
5 while y*y != x:
6 y =(y + x/y) / 2
7 return y:
Für den oben aufgeführten Pythoncode können Tests mit Hilfe des Python-Moduls "unittest" geschrieben werden (siehe auch Übungsaufgaben). Wir erklären hier die wichtigsten Befehle aus diesem Modul. Wir implementieren eine Testfunktionen (diese muss, wie im Python-Handbuch beschrieben, Methode einer Testklasse sein).
class SqrtTest(unittest.TestCase):
def testsqrt(self):
...
Zunächst muss man prüfen, ob die Vorbedingung korrekt getestet wird, d.h. ob bei einer negativen Zahl x eine Exception ausgelöst wird; dafür benötigt man
self.assertRaises(ValueError, sqrt, -1)
Sollte keine Exception vom Type ValueError ausgelöst werden, dann würde der Test hier einen Fehler signalisieren. Dieser Test funktioniert aber.
Weiter testen wir einige Beispiele, deren Wurzel wir kennen:
self.assertEqual(sqrt(9),3)
Wäre hier das Ergebnis ungleich 3, würde ebenfalls ein Fehler signalist, aber es funktioniert in un.serem Falle. Der Tests
self.assertEqual(sqrt(1),1)
schlägt mit ZeroDivisionError fehl! Wir sehen, dass in Zeile 4 eine Ganzzahldivision durchgeführt wird, deren Ergebnis stets abgerundet wird, was hier zu y = 0 und damit zum Fehler in Zeile 6 führt. Wieso hat dann aber der erste Test sqrt(9) == 3 funktioniert? Hier gilt x / 2 == 4 und x / y == 2 (jeweils nach Abrunden), und der Mittelwert der beiden Schätzungen ist gerade y == 3, also zufällig das richtige Ergebnis. Allgemein sehen wir jedoch, dass es nicht korrekt ist, mit ganzen Zahlen zu rechnen. Wir müssen also den Input zunächst in einen Gleitkommawert umwandeln:
1 def sqrt(x):
1a x = float(x)
2 if (x<0):
3 raise ValueError("sqrt of negative number")
4 y = x / 2
5 while y*y != x:
6 y =(y + x/y) / 2
7 return y:
Jetzt funktionieren die vorhandenen Tests, aber bei anderen Zahlen (z.B. x = 1.21) läuft das Programm in eine Endlosschleife. Dies liegt daran, dass durch die beschränkte Genauigkeit der Gleitkomma-Darstellung selten exakte Gleichheit in der while-Bedingung erreicht wird. Man darf nicht auf Gleichheit prüfen, sondern muss den relativen Fehler beschränken:
1 def sqrt(x):
1a x = float(x)
2 if (x<0):
3 raise ValueError("sqrt of negative number")
4 y = x / 2
5 while abs(1.0 - x / y**2) > 1e-15: # check for relative difference
6 y =(y + x/y) / 2
7 return y:
Jetzt terminiert das Programm, aber der Test
self.assertEqual(sqrt(1.21)**2, 1.21) # schlägt fehl
schlägt wegen der Gleitkomma-Rundung fehl. Man umgeht dieses Problem, indem man nur noch nähreungsweise Gleichheit fordert, z.B. auf 15 Dezimalstellen genau (bei 16 Dezimalen würde es nicht mehr funktionieren):
self.assertAlmostEqual(sqrt(1.21)**2, 1.21, 15)
Wenden wir jetzt das Prinzip der Condition Coverage an (siehe unten), sehen wir, dass die while-Bedingung bei allen bisherigen Tests zunächst mindestens einmal true gewesen ist. Ein weiterer sinnvoller Tests ist deshalb einer, der diese Bedingung sofort false macht. Dies trifft z.B. bei x == 4 zu, weil y = x / 2 hier gerade die korrekte Wurzel liefert. Wir fügen deshalb den Test
self.assertEqual(sqrt(4), 2)
hinzu, der erfolgreich verläuft. Das Prinzip der Domänen-Zerlegung (siehe unten) führt uns weiter dazu, die Wurzel aus Null als sinnvollen Test zu betrachten, weil die Null am Rand des erlaubten Wertebereichs liegt. Der Test
self.assertEqual(sqrt(0), 0) # schlägt fehl
schlägt in der Tat mit einem ZeroDivisionError fehl: In der Abfrage der while-Bedingung wird jetzt durch y == 0 geteilt. Wir können diesen Fehler beheben, indem wir die Division aus der Bedingung eliminieren:
1 def sqrt(x):
1a x = float(x)
2 if (x<0):
3 raise ValueError("sqrt of negative number")
4 y = x / 2
5 while abs(y**2 - x) > 1e-15*x: # check for relative difference without division
6 y =(y + x/y) / 2
7 return y:
Damit ist auch dieses Problem behoben. Wir sehen also, wie das systematische Testen uns dabei hilft, Fehler im Programm zu finden und zu eliminieren.
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
