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)

D1a: wenn gilt

P {Q} R und R ⇒ S

dann gilt auch

P {Q} S

D1b: 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 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 ust richtig" 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.

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 Matrixmultipölikation (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 α ∈  <math>{1,0}^N </math>  

(2) Matrixvektormultiplikation

    <math>\beta = \beta*\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>

 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. 

Nachteil formale Methoden

det. Verfahren vs randomisiertes Verfahren

Bsp. für Vollzug der testverfahren

fehlerhafter Pythoncode:

Prinzip der Domain Partitioning

Prinzip Code Coverage[3]

       - statement caverage : jedes Statement wird durch min. einen Test ausgeführt

       - conation caverage  : jede if. Abfrage sollte min. einmal mit true und einmal mit false durchlaufen werden
       
       - past caverage      : jeder Pfad (

Anwendung der Prinzipien auf den Pseudo- Code -> verbesserter Code