Korrektheit

23. April Achtung: Work in Progress!

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 durchführt, kommt man ins Zustand r.

Die Hoare-Logik besteht aus 5 Axiomen:

 D0: Axiom der Zuweisung
 R[t] {x=t} R[x]

 D1: Rule of Consequence (besteht aus zwei Axiomen)
 [beispiele unvollständig, beziehen sich jeweils nur auf p/r]
 # wenn P{Q}R und R=>S dann P{Q}S
 bspw. wenn (x<0) und (x<0)=>(x<5)

dann (x<5)

 # wenn P{Q}R und S=>P

dann S{Q}R

 bspw. wenn (x>5) und (x>5)=>(x>0)

dann (x>0)

 D2: Rule of Composition
 wenn P{Q_1}R_1 und R_1{Q_2}R 

dann P{Q_1, Q_2}R

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

 D3: Rule of Iteration
 wenn P[logisches_und]B{S}P

dann P{while B do S}[logisches_nicht]B[logisches_und]P

 Das heisst: [kommt noch]

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. [schau in deinen ANA-Unterlagen nach]

 A1: Kommutativität
 A2: Assoziativität
 A3: Distributivität
 A4: Substraktion
 A5: Neutrale Elemente

(Halb-)Automatisches Verfeinern

Dieses Verfahren ist beliebter, als das (Halb-)automatische Beweisen.

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[3]? 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 "Fraivaldsalgorithmus" von Hrmkowic anzuschauen bzw durchzuführen.

gegeben:

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

1 wähle Zufallsvektor 2 3

     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 Codee Caverage

       - statement caverage
       - conation caverage
       - past caverage

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