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 richtigen Ergebnisse liefert (in der Spezifikation wird die Vorbedingung (was vor der Anwendung des Algorithmus gilt) und die Nachbedingung (was nach der Anwendung des Algorithmus gilt) angegeben). Hier geht es ausschliesslich um die Prüfung der Korrektheit eines Algorithmus.

Nebenbemerkung (1): es gibt Algorithmen, die nie mit einer 100-prozentigen Wahrscheinlichkeit richtige Ergebnisse liefern können (z.B. nichtdeterministische Primzahltests). Nebenbemerkung (2): Korrektheit ist oft kein eigenständiges Kapitel in der Informatik, sondern wird meist unter dem Stichwort 'Softwaretest' geführt.

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 ===== Syntaktische Prüfung =

Es wird eine Grammatik definiert, deren Regel der Algorithmus befolgen muss. Für ein Programm heisst das beispielsweise, dass die Syntax der Programmiersprache eingehalten sein 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 [s. Dreieck erste Vorlesung]. Wenn man innerhalb des Algorithmus mit Typen arbeitet, muss man sicherstellen, dass gewisse semantische Bedingungen eingehalten 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), 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)

ein axiomatisiertes Programmiermodell

subset einer vorhandenen Programmiersprache, ein endlicher Automat, ein WHILE-Programm [s. erste Vorlesung] oder eine funktionale Programmiersprache

Der Beweis wird mit dem Hoare-Kalkül (Hoare-Logik) durchgeführt (Hoare erfand u.a. den Quicksort-Algorithmus). 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.

 Vorbedingung:
 int x,y
 0<y<x

 Gesucht:
 Quotient q, Rest r

 Algorithmus:
 r=x
 q=0
 while y<=r
   r=r-y
   q=q+1

 Nachbedingung:
 x==r+y*q und r<y

Aufbau der Hoare-Logik

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.

Die Hoare-Logik besteht aus 5 Axiomen:

 D0: Axiom der Zuweisung (Assignment Axiom)
 R[t] {x=t} R[x]
 bspw. t==5 {x=t} x==5

 D1: Konsequenzregel (Rule of Consequence, besteht aus zwei Axiomen)
 (a) wenn P{Q}R und R=>S 
 dann P{Q}S
 (b) wenn P{Q}R und S=>P
 dann S{Q}R
 bspw. wenn (x>5) und (x>5)=>(x>0) dann (x>0)

 D2: Sequenzregel (Rule of Composition)
 wenn P{Q1}R1 und R1{Q2}R 
 dann 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 P∧B{S}P
 dann P{while B do S}¬B∧P
 P wird dabei als Schleifeninvariante bezeichnet

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: Substraktion (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 (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)

(Halb-)Automatisches Verfeinern

Dieses Verfahren ist beliebter, als das (Halb-)automatische Beweisen. Die formale Spezifikation wird nach bestimmten Transformationsregeln in ein ausführbares Programm umgewandelt. Mehr dazu z.B. in der Wikipedia (Program refinement).

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? 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 "Freivaldsalgorithmus" von Hrmkowic anzuschauen bzw durchzuführen.

gegeben:

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

(1) Pseudo-Code

      wähle Zufallsvektor α ∈  {1,0}  

(2) Matrixvektormultiplikation

    β=βα       
 	     } A (Bα)
    γ=Aβ
    
    δ=Cα

(3) return γ==δ

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

  bei δ:
   

<math>

 \begin{pmatrix} 
   C_{11} & C_{12}  \\ 
   C_{21} & C_{22}  
 \end{pmatrix} 

</math>, <math>

 \begin{bmatrix} 
   α_{1}  \\ 
   α_{2}  
 \end{bmatrix} 

</math>,<math>

 \begin{bmatrix} 
   δ_{1}  \\ 
   δ_{2}  
 \end{bmatrix} 

</math>,

     Fall 1
     Fall 2
            a)
            b)
            c)

 Wahrscheinlichkeit q 
 Folgerung

Nachteil formale Methoden

det. Verfahren vs randomisiertes Verfahren

Bsp. für Vollzug der testverfahren

fehlerhafter Pythoncode:

Prinzip der Domain Partitioning

Prinzip Code Coverage

       - 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