Inhalt:

4. Kapitel: "Writing correct Programs"

5. Kapitel: A Small Matter of Programming

4. Chapter: writing correct programs

1. Die Herausforderung der Binären Suche

Als Motivation, sich so eingehend mit der binären Suche zu beschäftigen, sei erwähnt, daß nur 10% einer Gruppe von Studenten, die in ein paar Stunden die bin. Suche in einer Sprache ihrer Wahl programmieren sollten, keine Bugs in ihren Programmen hatten.

Analog dazu: 1946 wurde die erste bin. Suche veröffentlicht, aber erst 1962 die erste ohne Bugs.

Die Aufgabenstellung:

Wir sollen herausfinden, ob die gesuchte Zahl t (target=Ziel) in dem sortierten Array x[0..n-1] enthalten ist.

Präzisiert: Wir wissen dass n>=0 und dass x[0]<=x[1]<=x[2]<=...<=x[n-1]. Sollte n=0 sein ist das Array leer. Die Datentypen von t und den Elementen im Array sind gleich (damit vergleichbar). Der Code sollte für Integer-, Float- und String-Typen funktionieren. Die Antwort wird in der Integer-Variablen p (position) gespeichert:

p=-1 -> t ist nicht im Array x[0..n-1] sonst: 0<=p<=n-1 und t=x[p].

Die bin. Suche löst das Problem, indem sie das Array, das t enthalten kann eingrenzt. Initial ist das mögliche Array das gesamte Array. Nun wird t mit dem Element in der Mitte verglichen und somit das mögliche Array halbiert. Dieser Prozeß wird fortgesetzt bis t gefunden ist oder bis das mögliche Array, in dem t liegen kann, leer ist. Bei n Elementen im Array braucht die bin. Suche log₂n Vergleiche.

 

Zurück zum Inhaltsverzeichnis

 

2. Schreiben des Programms

Grundidee: Wenn t irgendwo in x[0..n-1] enthalten ist, dann innerhalb der Grenzen (range) von x. Kurzschreibweise: mustbe(range).

 

Die Programmskizze:

intialize range to 0..n-1
loop
/* invariant: mustbe(range) */
if range is empty,
break and report that t is not in the array
compute m, the middle of the range
use m as probe to shrink the range
if t is found during the shrinking process,
break and report ist position

Erläuterungen und Ausbau :

• Invariant: gilt am Anfang und am Ende jedes Schleifendurchlaufs, verdeutlicht die intuitive Formulierung (s.o.).
• Range: Wir präzisieren die Angabe durch zwei Indices l (lower) und u (upper) um den Bereich l..u darzustellen.
• mustbe(l..u) heißt also, dass wenn t im Array enthalten ist, dann im geschlossenen Interval x[l..u].
• Initial werden l und u offensichtlich auf 0 und n-1 gesetzt, was genau das ausdrückt, was wir zu Beginn wissen.
• Empty: Der Bereich l..u ist leer, wenn l>u, d.h. wir speichern -1 in p.
• m (Mitelpunkt zum Vergleich): m(l+u)/2
• Nun soll t mit x[m] verglichen werden und die passende Aktion erfolgen.
• Der Fall x[m]==t ist leicht: wir setzten p auf m und beenden die Schleife.
• Wenn x[m]<t, d.h. x[0]<=x[1]<=...<=x[m]<t, also kann t allenfalls noch im Bereich x[0..m] liegen. Da t nicht außerhalb von x[l..u] liegen soll folgern wir, dass es in x[m+1..u] liegt und schreiben dies als mustbe(m+1,u). Um die invariante Behauptung zu erhalten setzten wir also l=m+1.
• Wir hoffen, das der dritte Fall symmetrisch zum zweiten folgt.

 

Fertige Programmskizze:

l=0; u=n-1;

loop

/* invariant: mustbe(range) */

if l>u

p=-1; break;

m=(l+u)/2;

case

x[m]<t: l=m+1;

x[m]==t: p=m; break;

x[m]>t: u=m-1;

 

Bemerkungen:

Die präzise Invarianz, die durch den ganzen Vorgang aufrecht erhalten wurde, hat uns bei der Entwicklung des Codes sehr geholfen.

Diese gibt und jetzt einiges Vertrauen in die Richtigkeit des Programms, aber wir sind von seiner Korrektheit noch nicht überzeugt.

 

Zurück zum Inhaltsverzeichnis

 

3. Verifikation der Binären Suche

Die Programmskizze:

/* mustbe(0, n-1) */

l = 0; u = n-1;

/* mustbe (l, u) */

loop

/* mustbe(l, u) */

if (l > u)

/* l > u && mustbe(l, u) */

/* t is not in the array */

p = -1; break;

/* mustbe(l, u) && l <= u */

m = (l+u) / 2

/* mustbe(l, u) && l <= m <= u */

case

x[m] < t:

/* mustbe(l, u) && cantbe(0, m) */

/* mustbe(m+1, u) */

l = m+1;

/* mustbe(l, u) */

x[m] == t:

/* x[m] == t */

p = m; break;

x[m] > t:

/* mustbe(l, u) && cantbe(m, n) */

/* mustbe(l, m-1) */

u = m-1;

/* mustbe(l, u) */

/* mustbe(l, u) */

Verifikation:

Diese Analyse der Korrektheit verläuft nach dem bottom-up Verfahren, d.h. wir sehen uns die einzelnen Zeilen des Programms an und verfolgen, wie sie zusammenarbeiten, um das Problem zu lösen.

• Zeile 1-3:

Zeile 1 wahr aufgrund der Definition von mustbe.

Zeile 2 ergibt die Behauptung in Zeile 3.

• Zeile 4-27:

Die Argumentation besteht aus drei Teilen:

• Initialization:

Die invariante Bedingung ist bei der ersten Ausführung der Schleife wahr, da die Kommentare in 3. und 5. Zeile gleich sind.

• Preservation:

Wenn die invariante Bedingung am Anfang der Iteration gilt, dann wird sie zum Ende des Schleifendurchlaufs wieder wahr sein.

(Zeile 5 bis 27: denn Kommentare in Zeile 27 und 5 sind gleich!)

• Termination:

Die Schleife terminiert und das Ergebnis wird festgehalten (in p). Diesen Sachverhalt zu begründen benötigt die Invarianz.

(Zeile 9 und 21 (break-Statements)!)

Ein erfolgreicher Test in Zeile 6 führt automatisch zu der Bemerkung in Zeile 7. Dies wiederum impliziert die Aussage in Zeile 8. Wir setzten also korrekterweise p auf -1 und beenden die Schleife in Zeile 9.

Falls der Test in Zeile 6 nicht bestanden wird, gelangen wir in Zeile 10. Die Invarianz gilt immer noch (denn wir haben ja auch nichts daran geändert) und aufgrund des Tests wissen wir: l<=u. Zeile 11 ermittelt den Mittelpunkt des Arrays (abgerundet auf die nächste ganze Zahl). Diese Zahl liegt immer zwischen l und u (auch das Abrunden kann daran nichts ändern) also Zeile 12.

Die Analyse des case-Statements:

Der einfachste Fall ist der Zweite in Zeile 19: aufgrund des Testergebnisses (Zeile 20) ist es korrekt, p auf m zu setzten und die Schleife zu beenden. (Damit ist die korrekte Terminierung nachgewiesen!)

Aufgrund der vorangegangenen Konzentration (beim Entwickeln) auf den ersten Fall, betrachten wir nun den Dritten. Der zweite ist, wie gesagt, symmetrisch.

In Zeile 23 sind zwei wichtige Beobachtungen vermerkt: die Erste ist die Invarianz, die nicht verändert wurde, die Zweite ist wahr, da wir wissen, dass t<x[m]<=x[m+1]<=...<=x[n-1]. Also wissen wir, dass t nicht oberhalb einer Arrayposition von m-1 stehen kann. Logische Schlußfolgerung ist, dass t (wenn überhaupt) zwischen l und m-1 stehen muß. (=Zeile 24). Die Anweisung in Zeile 25 ergibt, dass unter der (wahren) Bedingung in Zeile 24 Zeile 26 resultiert.

Damit ist die Invarianz in Zeile 27 korrekt!

 

Wir haben also gezeigt:

Wenn die Schleife terminiert, dann mit dem korrekten Ergebnis in p. (keine Unendlich-Schleife)

 

Noch nachzuweisen ist, dass das Array tatsächlich verkleinert wird (=> Terminierung)

Initial ist das Array n Elemente groß. Zeile 6-9 legen fest, dass die Schleife terminiert, wenn das Array weniger als ein Element hat. Beide Case-Anweisungen, die nicht direkt terminieren, schließen m selbst im neuen Array aus; damit wird die Größe mindestens um 1 Element verringert. Das Programm hält also zwangsläufig irgendwann an.

 

Zurück zum Inhaltsverzeichnis

 

4. Prinzipielles zu Verifikations-Techniken

Der vorangegangene Abschnitt war sehr detailiert, in der Praxis würde man wohl weniger formal arbeiten, aber gerade diese Details zeigen uns einige generelle Prinzipien:

• Assertion (=Behauptung):

Eine Beziehung zwischen Input, Programmvariablen und Output, die den Zustand des Programms beschreibt. Die Behauptung ermöglicht es dem Programmierer diese Relation präzise zu formulieren.

• Sequential Control Structures (=Kontrollstruktur für sequenzielle Programmteile):

Die einfachste Form der Kontrolle eines Programms: "Tue dies und danach das". Wir verstehen diese Strukturen, indem wir Bemerkungen (Kommentare) einfügen, um Schrittweise die Arbeit des Programms nachzuvollziehen.

• Selection Control Structures (=Kontrollstruktur für selektive Programmteile):

Hier werden z.B.: if- und case-Anweisungen behandelt:

Wir zeigen die Korrektheit jeder einzelnen Auswahlmöglichkeit einzeln.

Aufgrund der Auswahl können wir eine weitere Voraussetzung machen.

• Iteration Control Structures (=Kontrollstruktur für iterative Programmteile):

Hier werden Schleifen behandelt:

Wir müssen zeigen, dass die Schleifeninvarianz durch die Initialisierung korrekt ist.

Dann zeigen wir, dass jede Iteration ihre Korrektheit erhält. (Induktion). Danach muß begründet werden, dass, wenn die Schleife terminiert, das Ergebnis richtig ist.

• Functions:

Um eine Funktion zu verifizieren, stellen wir sie zuerst durch zwei Bedingungen dar:

• Precondition: Muß als Voraussetzung gelten, bevor die Funktion aufgerufen wird.
• Postconditon: Das Ergebnis, das die Funktion bei Terminierung liefert.

Wenn eine Funktion unter Precondition aufgerufen wird, so wird sie garantiert die Postcondition liefern. Ist dies einmal nachgewiesen, so kann diese Relation zwischen Pre- und Postcondition benutzt werden, ohne die explizite Implementierung zu nutzen.

Bemerkungen:

• Die Verifikation gibt dem Programmierern die "Sprache", in der sie ihr Verstehen ausdrücken können.
• Es ist enorm hilfreich, eine Invarianz für jede Schleife zu erstellen.
• Die wirklich wichtigen Erklärungen enden im Programm als Kommentare.
• Ein einfacher Code ist meist der richtige Weg zur Korrektheit.
• An schweren Passagen benutzt man die Formalismen, um Fehler zu Vermeiden und den Überblick zu behalten, aber an vermeintlich einfachen Stellen verfällt man wieder ins "einfach Programmieren - dann Fehler raustesten"

 

Zurück zum Inhaltsverzeichnis

 

5. Probleme und Beispiele
• Prinzipiell muß man auch noch prüfen, ob andere Fehler Auftreten könnten, wie z.B.: eine Division durch 0, ein overflow in den Variablen (Wertebereich - z.B. Integer - überschritten) und ob auf nicht existente Arrayelemente zugriffen wird.
• Bei einer rekursiven Formulierung der binären Suche verläuft die Argumentation der Verifizierung analog

 

Zurück zum Inhaltsverzeichnis

 

 

 

1. Vom Pseudocode zu C

Die Variable t und die Inhalte des Arrays sind vom selben Datentyp (und damit vergleichbar).

Typedef int DataType;

Das Array wird durch zwei globale Variablen dargestellt:

int n;

DataType x[MAXN];

• Die meisten Pseudocode-Anweisungen können zeilenweise übersetzt werden.
• Die Pseudo-Anweisung, einen Wert in p zu speichern, wird durch eine Return-Anweisung ersetzt.
• Die Pseudocode-Schleife wird zuerst zu der Endlosschleife

for(;;) {

if (l > u) return -1;

....... (Rest des Schleifenkörpers) ....

Dies kann man aber vereinfachen zu:

while (l <= u) {

....... (Rest des Schleifenkörpers) ....

}

return -1;

 

 

Der komplette Code in C:

int BinSearch (DataType t)

/* return (any) position if t is in sorted x[0..n-1] or -1 if t is not present */

{

int l, u, m;

l = 0;

u = n-1;

while (l <= u) {

m = (l+u) / 2

if ( x[m] < t) l = m+1;

else if ( x[m] == t) return m;

else /* x[m] > t*/ u = m-1;

}

return -1;

}

 

Zurück zum Inhaltsverzeichnis

 

2. Ein Härtetest

Grundidee: Erstmal ein paar Test per Hand durchführen. Einfache Fälle (null-, ein- und zwei-elementige Arrays) ergeben oft schon erste Bugs.

Erstelle einen "Driver", der die Funktion aufruft. (Driver in die Main-Methode einfügen)

Der Driver:

while (scanf(``%d %d``, &n, &t) != EOF) {

for (i=0; i<n; i++) x[i] = 10*i;

printf(`` %d\n``, BinSearch(t));

}

Test und Ergebnisse:

• Wir starten den Test mit dem Driver in der main-Funktion und BinSearch als Funktion.
• Eingaben (n und t) kursiv.
• Ergebnis der bin. Suche normal.

 

2 0

0

2 10

1

2 -5

-1

2 5

-1

2 15

-1

• Beim ersten Aufruf wird ein 2-elementiges Array erzeugt mit x[0]=0 und x[1]=10. Die bin. Suche findet die 0 in Position 0.
• Beim zweiten Aufruf wird dasselbe Array erzeugt. Die bin. Suche findet die 10 in Position 1.
• Die nächsten 3 Aufrufe beschreiben nicht erfolgreiche Suchen (korrekte).

Bemerkung:

• Bei den meisten fehlerhaften Programmen wurde die Vergleichsvariable m nicht aus dem Bereich des nächsten (kleineren) Arrays ausgeschlossen, wenn z.B.: für zwei-elementige Arrays immer wieder mit demselben Array verglichen wird (unendlich)
• Meist günstiger als Debugging-Tools sind Kontrollausgaben (print-Statements), um Fehler verstehen und beheben zu können (man sieht was schon bearbeitet wurde und was noch nicht)

 

Zurück zum Inhaltsverzeichnis

 

3. Die Kunst der Behauptungen

Behauptungen spielen eine wichtige Schlüsselrolle: sowohl bei der Entwicklung des Codes (Kap 4) wie auch später noch. Sie erlauben uns auf ihre Korrektheit zu schließen. Wir werden sie nun in den Code einbinden um sicherzustellen, dass die Laufzeit sich so verhält wie wir vermuten.

 

Wir benutzen die assert-Anweisung um auszudrücken, dass der logische Ausdruck wahr ist.

else if (x[m] == t) {

assert (x[m] == t);

return m;

} else ...

Dies würde aber nur die Anweisung in der Abfrage wiederholen, also bauen wir die assert-Anweisung weiter aus:

assert (0<=m && m<n && x[m] == t);

 

Wenn die Schleife terminiert, ohne t gefunden zu haben, wissen wir, dass l und u sich gekreuzt haben, das Array also leer ist.

assert (x[u] < t && x[u+1] > t);

return -1;

Vorsicht: falls n=0 ist u=n-1 nicht als Array-Index definiert

assert ((u < 0 t x[u] < t) && (u+1 >= n t x[u+1] > t));

 

Wir haben bewiesen, dass die Suche immer anhält, da der Bereich des Arrays verkleinert wird. Dies können wir auch während der Ausführung testen:

Initial: size = n+1;

Nach For: oldsize = size;

size = u-l +1;

assert (size < oldsize);

 

Ähnlich kann man auch testen, ob das Array sortiert ist:

Funktion: int sorted()

{ int i;

for (i=0; i<n; i++)

if (x[i] > x[i+1]) return 0;

return 1;

}

Test: assert (sorted());

 

Bemerkungen:

• Mit diesem Test in der main-Schleife kann das Ergebnis der bin. Suche in einer Zeit proportional zu n*log(n) ermittelt werden.
• Assertions sind besonders hilfreich während des Tests in seinem Gerüst und wenn man Komponenten in ein System einbinden will.
• Einige Projekte (Programmierumgebungen) beachten beim compilieren die assert-Anweisungen nicht (ähnlich wie Kommentare), so dass diese keine Laufzeit auf sich ziehen.

 

Zurück zum Inhaltsverzeichnis

 

4. Automatisches Testen

Der nächste Schritt ist nun ein Gerüst zu erstellen, das das Programm testet.

/* testet nur unterschiedliche Elemente (plus ein weiteres am Ende des Arrays) */

for i = [0,n]

x[i] = 10*i;

for i = [0, n)

assert (BinSearch(10*i) == i);

assert (BinSearch(10*i - 5) == -1);

assert (BinSearch(10*n - 5) == -1);

assert (BinSearch(10*n) == -1);

Die Assert-Anweisungen testen jede mögliche Position für eine erfolgreiche und nicht erfolgreiche Suche. Der Fall, dass ein Element im Array ist, aber bei der Suche nicht beachtet wird, ist ebenfalls enthalten.

 

/* testet gleiche Elemente */

for i = [0,n)

x[i] = 10;

if (n == 0) assert (BinSearch(10) == -1);

else assert (0 <= BinSearch(10) && BinSearch(10) < n);

assert (BinSearch(5) == -1);

assert (BinSearch(15) == -1);

 

Zurück zum Inhaltsverzeichnis

 

5. Laufzeit

Wir erstellen nun ein Programm, das die Laufzeit verdeutlichen soll.

 

while read(algnum, n, numtest)

{

for i=[0, n)

x[i] = i;

starttime = clock();

for testnum = [0, numtest)

switch (algnum)

case 1: assert (BinSearch1(i) == i);

case 2: assert (BinSearch2(i) == i);

cicks = clock() - starttime;

print algnum, n, numtestn clicks,

clicks/(1e9 * CLOCKS_PER_SEC * n * numtest)

}

 

Bemerkungen:

• Dieser Code ermittelt die durchschnittliche Laufzeit einer erfolgreichen bin. Suche in einem n-elementigen Array.
• Man sollte immer mehrere Algorithmen testen.

 

Tests und Ergebnisse:

1 1`000 10`000

1 1`000 10`000 3445 344,5

1 10`000 1`000

1 10`000 1`000 4436 443,6

1 100`000 100

1 100`000 100 5658 565,8

1 1`000`000 10

1 1`000`000 10 6619 661,9

 

• Es wird nur der vorgestellte Algorithmus der binären Suche getestet, aber im Allgemeinen ist es günstig, mehrerer Algorithmen gegeneinander zu testen.
• In jedem Schritt wird n um den Faktor 10 vergrößert, t hingegen um denselben Faktor verkleinert.
• Die letzte Ziffer gibt die durchschnittliche Kosten de Suche in Nanosekunden an.
• Die Laufzeit scheint also hiermit: 50 + 30*log₂(n) Nanosekunden zu sein.

 

Zurück zum Inhaltsverzeichnis

 

6. Fazit

 

• Wir haben den Pseudocode vorsichtig entwickelt.
• Analytische Techniken benutzt um seine Korrektheit nachzuweisen
• Zeilenweise in C übersetzt
• Das Output-Verhalten beobachtet
• Assertions in den Code eingebunden, um die theoretische Analyse mit dem praktischen Verhalten zu vergleichen
• Maschinell mit Tests bombardiert
• Abschließend die Laufzeit gezeigt

 

Aber:

Wir können nicht absolut sicher sein, ob

• Der Aufruf mit einem sortierten Array erfolgt
• -1 das gewünschte Ergebnis für erfolglose Suche ist
• das gesuchte Element mehrfach im Array vorkommt. Dann gibt dieser Code irgend eine Position zurück. Ist das gewünscht?

 

Zurück zum Inhaltsverzeichnis