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

1. es gibt Algorithmen, die nie mit einer 100-prozentigen Wahrscheinlichkeit richtige Ergebnisse liefern können (z.B. nichtdeterministische Primzahltests).
2. 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ß 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 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 dafür, dass ein Test einen vorhandenen Fehler übersieht, am Bespiel des Algorithmus von Freivalds studieren. Es handelt sich dabei um einen randomisierten Algorithmus zum Testen der Matrixmultiplikation (siehe J. Hromkovič: "Randomisierte Algorithmen", Teubner 2004).

gegeben:

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

(1) Pseudo-Code

      wähle Zufallsvektor der Länge N aus Nullen und Einsen: <math>\alpha \in \{0, 1\}^N </math>  

(2) Matrixvektormultiplikation

    <math>\beta = B*\alpha</math>          |
                     ->  <math> A*(B\alpha)</math>
    <math>\gamma=A*\beta</math>          |
    
    <math>\delta=C*\alpha</math>

(3)

       return   γ==δ

[hier wird sich nun angeschaut, mit welcher Wahrscheinlichkiet der Alg. den Fehler findet, wenn es einen gibt; true: wenn es keinen Fehler gibt] also:

Wahrscheinlichkeit p, dass FA Fehler findet oder Wahrscheinlichkeit q, dass FA Fehler nicht findet

bei δ (geschieht folgendes):

    C= <math>(c_{11} c_{12} c_{21} c_{22} )</math>   <math>\alpha=(\alpha_1 \alpha_2)</math> <math>\delta=(\delta_1 \delta_2)</math> 

Fallunterscheidung:
     
     Fall 1  C enthält genau 1 Fehler
                   z.B. <math>c_{11}</math> mit falschem Wert
                   allg. gilt noch :
                   <math>\delta_1 = c_{11}\alpha_1 + c_{12}\alpha_2</math>
                   <math>\delta_2= c_{21}\alpha_1 + c_{22}\alpha_2</math>
                   Fehler gefunden, wenn <math>\delta_1</math> falsch <math>\Leftrightarrow\alpha_1\not=0</math>  ;
                   p =<math>\frac{1}{2}</math>= q
      
     Fall 2  C enthält 2 Fehler
             
     a)        in verschiedenen Zeilen und Spalten
               z.B. <math>c_{11}+c_{21}</math>
              
               <math>q_1= \frac{1}{2}</math>, <math>q_2=\frac{1}{2}</math>
               <math>\alpha_1\not=0</math>   ,<math>\alpha_2\not=0</math>
               <math>\rightarrow</math> <math>q_1*q_2 = \frac{1}{2}* \frac{1}{2} = \frac{1}{4}</math>          

<math>\alpha_1</math> und <math>\alpha_2</math> sind unabhängig voneinander. Wenn kein Fehler gefunden wird, dann sind <math>\alpha_1,\alpha_2=0</math>. Die Wahrscheinlichkeit allerdnings liegt nur bei <math>\frac{1}{4}</math>. Die Wahrscheinlichkeit das ein <math>\alpha=0</math> ist, liegt bei <math>\frac{3}{4}</math>.

      b)       in verschiedenen Zeilen, gleiche Spalten 
               z.B <math>c_{11} + c_{21}</math>  ( abhängig von <math>\alpha_1</math>)
               Fehler <math>\leftrightarrow\alpha_1\not=0</math>,   <math>q=\frac{1}{2}</math>
              
      c)       2 Fehler in der gleichen Zeile
               z.B. für <math>c_{11}+c_{12}</math> gilt:
               <math>\delta_1=\alpha_1*c_{11}+\alpha_2c_{12}</math>
               Hier treten nun zwei ungünstige Fälle auf: 
                               1) Der Fehler wird u.a. nicht gefunden, wenn <math>\alpha_1, \alpha_2=0</math>. Dann ist 
                                  <math>q=\frac{1}{4}</math>
                               2) <math>\alpha_1=\alpha_2=1</math>, aber die Werte <math>c_{11}+c_{12}</math> sind 
                                  "zufälligerweise"so falsch, dass sie sich gegenseitig aufheben,
                                  d.h. falls <math>c_{11}+c_{12}=\gamma_1\Rightarrow q=\epsilon<\frac{1}{2}</math>

Ziel dieses Algorithmuses ist es H zu zeigen oder zu wiederlegen ohne die Matrizenmultiplikation anzuwenden.

 Es gilt der Satz:
     Die Wahrscheinlichkeit q, dass FA einen vorhandenen Fehler nicht findet, ist <<math>\frac{1}{2}</math>

 Folgerung: lässt man FA mit verschiedenen <math>\alpha</math> k-mal laufen, gilt <math>q_k< z^{-k}</math> konvergiert
  schnell gegen 0. 

Unterschied deterministischer und randomisierter Algorihtmus

Nachdem nun die formalen Methoden sowie der Software-Test vorgesellt worden sind, ist nun die Frage, welcher der beiden Vorgänge der bessere ist. Für die formalen Methoden sprechen, dass man mit ihnen beweisen kann, dass H nun entweder tatsächlich falsch oder richtig ist. Allerdings liegt hier auch einn nicht zu verachtendes aber vor, denn es ist keine 100 % Garantie gegeben, dass die formalen Methoden auch wirklich immer richtig sind ( z.b. Hardware im Weltall, die kosmicher Strahlung ausgesetzt ist-> unvorhergesehener Bitumfall). Zudem besitzen die formalen Methoden die Theoremigenschaft, dass sie einen längeren Zeitraum in Anspruch nehmen um den jeweiligen Test zu berechnen. Der Software-Test ist zwar in seiner Fehlersuche nicht allzu zuverlässig wie dei formalen Methoden, aber ist dessen Berechnungsphase wesenltlich schneller:

randomisiertes Algorithmen

      -sind schnell und einfach: -da die Operationen einfach sowie wenig Zeit kosten
                                 -des öfteren eine Auswahl vorgenommen wird ohne die Gesamtmenge näher zu betrachten
                                 -die Auswahl selbst erfolgt aufgrund einfacher Kriterien (bspw. zufällige Auswahl)
                                 
      -können Lösungen approximieren und liefern gute approximative Lösungen

deterministische Algorithmen[3]

     -bei jedem Programmaufruf werden immer die selben Schritte durchlaufen
     -keine Zufallswerte
     -komplexer Aufbau
     - unrealistische Durchlaufzeit, z.B. 20 Monate                             
    
     

Anwendung des Softwaretestverfahren

Beispeil an Python-Code

Man betrachte einen fehlerhafter Pythoncode:

          1      def sqrt(x):
          2      if(x<0):
          3      raise DomainError("sqrt of negative number")
          4      <math> y=\frac{x}{2}</math>
          5      <math> y=\frac{y+\frac{x}{y}}{2}</math>
          6      return y:

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

Es gilt nun den Pythoncode genauer zu betrachten:

Zur Stütze dienen zum ersten die Testfunktionen

       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>bekommt man hier nicht 3 als Ergebnis heraus, ebenfalls Fehlersignalisierung
       -assertEqual(sqrt(1),1)
   

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

Prinzip der Domain Partitioning[4]

   -hier wird die einzusetzende Zahl ausgewählt
   -man teilt die Werte, die sich im Algrithmus gleich verhalten, in Wertebereiche ein
   <math>\Rightarrow</math> 1) wähle aud jedem Intervall min einen repräsentativen Wert
      2) wähle aus jedem Intervall die Randwerte (diese sind interessant, weil 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
       - conation coverage  : jede if. Abfrage sollte min. einmal mit true und einmal mit false durchlaufen werden
       - past coverage      : jeder Pfad wird einmal durchlaufen [in der Praxis wird allerdning nur eine Näherung erreicht)

Anwendung der Prinzipien auf den Pseudo- Code

Den ersten Bug findet man, wenn man versucht Zeile5 anzuwenden. Bei Integer-Division wird abgerundet und 3 wird nicht als Endergebnis ausgegeben<math>\Rightarrow</math>Befehl einbauen, der in reelle Zahlen umwandelt.Zudem ist dann hier noch zu beachten, dass durch das einfügen eines float-Befehls Zeile 5 zu einer Endlosschleife wrd, da keine Gewissheit mehr gegeben ist, dass tatsächlich beides gleich ist Punkt 2) von 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 Errorfehlermedlung erhalten würde.

<math>\Longrightarrow</math> verbesserter Code

‎

Daraus ergeben sich 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]