Verifikation von Algorithmen (anhand von Biphrost)
Seit einiger Zeit hat sich nichts an Biphrost verändert, was vor allem daran lag, dass bisher keine neuen Features notwendig waren, die mit dem Gedanken von Biphrost vereinbar sind, d.h. Biphrost ist bisher vollständig. Aber ist Biphrost auch korrekt, d.h. macht Biphrost das, was vorgesehen ist? Ich habe keinerlei Unit-Tests verwendet, aber macht das einen Unterschied in Bezug auf Korrektheit? Nein, denn Unit-Tests können Fehler aufdecken, aber niemals deren Existenz widerlegen. Wie lässt sich die Korrektheit dann zeigen? Die Antwort ist entmutigend: Sie lässt sich im Allgemeinen nicht zeigen, was man sich am Halteproblem deutlich machen kann, denn wenn man nicht entscheiden kann, ob ein beliebiges Programm terminiert, wie soll man dann andere subtilere Eigenschaften zeigen? Allerdings sieht es dann doch nicht so düster aus, wie es den Anschein hatte: Es gibt immerhin noch unendlich viele Eigenschaften, die sich entscheiden lassen.
Wie geht es weiter? Zuerst möchte ich den wichtigsten und wahrscheinlich einzigen nicht-trivialen Algorithmus von Biphrost beweisen. Hierfür wird erstmal eine Aussage, d.h. Eigenschaft, benötigt, die bewiesen werden soll. Diese Eigenschaft lässt sich folgendermaßen formulieren:
Gegeben: Ein URI der Form x0/x1/.../xn-1 und ein Basispfad base, der auf / endet.
Gesucht: Die Datei base verkettet mit x0/x1/.../xk.php mit 0 ≤ k ≤ n-1 und maximalem k, d.h. die in der Ordnerstruktur tiefste Datei, die sich nach obigem Schema bilden lassen.
Für die Äquivalenz von maximaler Tiefe und maximalem k sind folgende Spezialfälle zu betrachten:
- Es existiert ein i ∈ {0, ..., n-1} mit: xi = ε, wobei ε das leere Wort darstellt ⇒ Es befindet sich im URI die Zeichenkombination //, die semantisch äquivalent zu / ist, was impliziert, dass es mehrere Variablen k geben kann, für die der zugehörige Pfad maximal tief ist. Folglich sind Widersprüche zur Äquivalenz möglich, z.B. ist der tiefste Pfad /foo/.php zu /foo// äquivalent, auch wenn es einen Pfad mit größerem k, z.B. /foo///, geben kann. Dies lässt sich allerdings verhindern, indem die Voraussetzung verschärft wird, d.h. dass alle für alle i gilt: xi ≠ ε.
- Es existieren genau m verschiedene Variablen i ∈ {0, ..., n-1} mit: xi = .. ⇒ Ist m > n-m, dann würde dies bedeuten, dass man sich oberhalb des Basispfads befindet, was sicherheitstechnisch bedenklich und alleine deshalb auszuschließen ist. Zudem würde dieser Fall einen Widerspruch zur Äquivalenz darstellen, z.B. wäre foo/bar tiefer als foo/bar/../../index trotz größerem k.
Aus dem ersten Spezialfall lässt sich folgende Äquivalenzen folgern bzw. einführen:
- Der gesuchte Pfad von x-1/x0/.../xn-1 (x-1 = ε) ist äquivalent zu dem von x0/.../xn-1, da base//x0/.../xk.php zu base/x0/.../xk.php äquivalent ist, folglich kann ein führender Slash entfernt werden.
- Der gesuchte Pfad von x0/.../xn (xn = ε) kann nicht äquivalent zu dem von x0/.../xn-1 sein, da base/x0/.../xn-1/.php im Allgemeinen nicht äquivalent zu base/x0/.../xn-1.php ist. Da eine Datei mit dem Namen ".php" jedoch wenig Sinn in diesem Kontext ergibt, führen wir diese Äquivalenz explizit ein. Ist k < n-1 unterscheiden sich die gesuchten Pfade hingegen nicht.
- Existiert im URI x0/.../xn-1 mindestens ein i mit 1 ≤ i ≤ n-2 (i = 0 und i = n-1 wurden bereits in den vorherigen Fällen betrachtet) und xi = ε, dann ist der zugehörige gesuchte Pfad äquivalent zu dem von x0/.../xi-1/xi+1/.../xn-1. Ist i < k, dann ist base/x0/.../xi-1//xi+1/.../xk.php äquivalent zum Pfad base/x0/.../xi-1/xi+1/.../xk.php, womit letztendlich doppelte Slashes zu einem ersetzt werden können ohne die Bedeutung zu gefährden. Ist i > k, können sich die gesuchten Pfade nicht unterscheiden. Bei Gleichheit von i und k tritt ein zum Fall 2 analoger Fall ein: base/x0/.../xi-1/.php müsste äquivalent zu base/x0/.../xi-1.php sein, damit die zu zeigende Äquivalenz weiterhin gilt. Da eine Datei mit dem Namen ".php" wenig Sinn ergibt, führen wir eine solche Äquivalenz abermals ein.
Um die Eindeutigkeit des Algorithmus zu sichern, ist es notwendig zu verhindern, dass Dateien mit dem Namen ".php" als Einstiegspunkte erkannt werden. Da dieser Fall jedoch im Kontext der Software unsinnig ist, wird auf eine explizite Überprüfung verzichtet.
Durch Klärung der Spezialfälle können wir o.B.d.A. davon ausgehen, dass der URI aus nicht-leeren xi mit xi ≠ ε besteht. Es bleibt zu zeigen, dass in diesem Fall ein maximales k der maximalen Tiefe entspricht und vice versa. Dieses lässt sich leicht aus der Monotonie der Beziehung zueinander folgern: Wird ein größeres k gewählt, muss lt. Voraussetzung .. ≠ xi ≠ ε jeder Schritt weiter in die Tiefe führen.
Zunächst betrachten wir den leicht modifizierten Algorithmus für Einstiegspunkte (die for-Schleife wurde durch eine semantisch äquivalente while-Schleife ersetzt):
$components = array_values(array_filter(explode('/', $uri)));
if(in_array('..', $components)) {
return false;
}
$n = count($components);
$dir = $this->base;
$result = false;
$i = 0;
while(file_exists($dir) && is_dir($dir) && $i < $n) {
$component = strtolower($components[$i]);
$file = $dir . $component . '.php';
$dir .= $component . '/';
if(file_exists($file)) {
$result = array($file, array_slice($components, $i+1));
}
$i++;
}
return $result;
Der zweite Spezialfall wird direkt nach dem Zerlegen des URIs in seine Komponenten abgehandelt. Existiert eine Komponente mit dem Wert "..", wird der Algorithmus abgebrochen, indem false zurückgegeben wird. Als Komponente wird nachfolgend jedes nicht-leere xi aus der Eingabe bezeichnet. Die Zerlegung in Komponenten erfolgt durch die Funktion explode. Leere Komponenten können nur entstehen, wenn mehrere Slashes innerhalb des Strings vorkommen oder ein Slash am Anfang oder am Ende des Strings steht. Der Algorithmus ist allerdings durch die Äquivalenzen so definiert, dass ein solcher URI zu einem URI umgeformt werden darf, der keine solche Arten von Slashes enthält. Somit ist sichergestellt, dass der Algorithmus das gleiche Ergebnis zurückgibt, wenn die leeren Komponenten einfach entfernt werden. Dieses Entfernen wird durch die Funktion array_filter mit nur einem Argument erreicht. Um die Indizes zu reinitialisieren, folgt noch der Aufruf array_values.
Anschließend folgen triviale Initialisierungen:
- Die Anzahl der Komponenten wird in n gespeichert.
- Die Variable dir wird mit base belegt.
- Die Variable result wird mit false belegt.
- Der Zähler i wird mit 0 belegt.
Zu diesen vier Variablen lassen sich invariante Eigenschaften angeben, die das Beweisen der Korrektheit vereinfachen sollen:
- Invariante: n bleibt konstant.
- Invariante: dir endet immer auf /.
- Wenn noch kein Einstiegspunkt bekannt ist, gilt result = false. Ansonsten ist result0 = base/x0/.../xk.php ein gültiger Einstiegspunkt (d.h. die Datei existiert!) und result1 = array(xk+1, ..., xn-1) stellt die nicht verarbeiteten Komponenten dar.
- Invariante: Für i gilt immer 0 ≤ i ≤ n und außerdem wird i immer um genau 1 inkrementiert.
Die Invarianten 1, 2 und 4 lassen sich trivialerweise zeigen:
- n wird nirgends verändert.
- ein / wird explizit ans Ende von dir geschrieben.
- i = 0 und i++ sind die einzigen Kommandos, in denen i verändert wird und die Schleife bricht spätestens bei i = n ab.
Aus den Invarianten 1 und 4 folgt die Termination der while-Schleife, da sie nach spätestens n Schritten abbricht.
Der Beweis für die dritte Invariante ist ein wenig aufwändiger. Eine wesentliche Eigenschaft von dir ist es, dass sie den Pfad zu einem möglichen Einstiegspunkt bis zur Komponente xi-1 enthält, d.h. dir enthält base/x0/.../xi-1/. Der mögliche Einstiegspunkt lässt sich dann mit dieser Eigenschaft als dirxi.php = base/x0/.../xi-1/xi.php angeben. Existiert dieser, dann wird er in result0 abgelegt und die nicht verbrauchten Komponenten sind in result1 enthalten. Dass das Zusammenstellen von result1 korrekt ist, lässt sich anhand der Beschreibung der Funktion array_splice sehen.
Die Äquivalenz von maximalem k und maximaler Tiefe lässt sich auf die Schleife anwenden, da das k (in diesem Fall i) in jedem Durchlauf erhöht wird. Somit ist bekannt, dass der zuletzt gefundene Einstiegspunkt tiefer als alle anderen Einstiegspunkte ist. Es bleibt also noch zu zeigen, dass nach Abbruch der Schleife keinen weiteren Einstiegspunkt geben kann. Bricht die Schleife ab, gilt die Negation der Schleifenbedingung, d.h. entweder existiert der Ordner dir nicht oder dir ist kein Ordner oder i = n. Ist i = n kann es keinen weiteren Einstiegspunkt geben, da bereits alle Komponenten verbraucht wurden. Existiert dir nicht oder ist es kein Ordner, kann man nicht weiter in die Tiefe gehen und somit keinen weiteren Einstiegspunkt mehr finden. Damit wurde letztendlich gezeigt, dass der Algorithmus korrekt ist, da er den gesuchten Einstiegspunkt zurückgibt. q.e.d.
Dieser Beweis war recht aufwändig für ein solch kurzes Stückchen Code. Das zeigt vor allem eines: Code zu beweisen ist häufig aufwändig. Anhand der verwendeten Argumente wird einem auch die Schwierigkeit klar, diese Verifikation zu automatisieren. Lt. Satz von Rice ist es gar unmöglich, einen Algorithmus zu finden, mit dem man dieses Prozedere für alle Eigenschaften automatisieren kann. Warum habe ich dennoch diesen Beweis geschrieben? Zum einen um sicherzustellen, dass Biphrost so korrekt wie möglich funktioniert und zum anderen weil mir dieses Thema derzeit großen Spaß bereitet. Allerdings musste ich beim Schreiben dieses Artikels feststellen, dass sich imperative Programmiersprachen für solche Unternehmungen nur mittels geeigneter Formalismen eignen, wie z.B. die Natural Semantics und Structual Operational Semantics. Ob sich Haskell-Code mittels Denotationeller Semantik besser beweisen lässt, werde ich in hoffentlich nicht allzu ferner Zukunft ausprobieren können.