Abstract:
Graphen und Graph-basierte Algorithmen sind allgegenwärtig. Aufgrund dieser Allgegenwärtigkeit, ist es wichtig, dass diese Algorithmen korrekt funktionieren. Um das zu gewährleisten, können die Graph-Algorithmen formal verifiziert werden. Deduktive Programm-Verifikation wird verwendet, um zu zeigen, dass ein Programm eine formale Spezifikation seines Verhaltens, für jede gültige Eingabe erfüllt, was keine triviale Aufgabe ist. Außerdem gibt es nicht nur eine Implementierung von Graphen. Diese können in einer Vielfalt von Datenstrukturen dargestellt werden, die alle ihre Vor- und Nachteile; z.B. ... mehrbezüglich Laufzeit oder Speicherverbrauch haben.
Es ist unklar, wo potentielle Engstellen im Verifikationsprozess auftauchen werden. Unter diesen Datenstrukturen gibt es besser und schlechter geeignete, wenn es um deduktive Programmverifikation von Graph-Algorithmen geht. Mit dem Wissen darüber, welche Datenstrukturen sich besser eignen um einen Graph-Algorithmus zu verifizieren, bekommt man eine zusätzliche Entscheidungshilfe beim Auswählen einer Implementierung.
In dieser Arbeit untersuchen wir dies für einen konkreten Algorithmus: Tiefensuche. Tiefensuche ist ein simpler Algorithmus, um einen Graphen zu traversieren. Viele komplexere Graph-Algorithmen basieren auf Tiefensuche. Somit ist die Verifikation von Tiefensuche, trotz seiner Einfachheit, von Interesse. Wir verifizieren zwei verschiedene Implementierungen von Tiefensuche in Graphen. Dazu verwenden wir die formale Spezifikationssprache JML, um Java-Programme zu spezifizieren, und das KeY-System für die deduktive Verifikation. Beide Implementierungen werden wir für vier Graph-Repräsentationen untersuchen. Die verwendeten Graph-Datenstrukturen sind Adjazenz-Matrizen, -Felder und -Listen, sowie eine verzeigerte Datenstruktur. Als Implementierung von Tiefensuche, verwenden wir eine rekursive Version, die rekursive Methodenaufrufe verwendet, und eine nicht-rekursive Version, die statt rekursivem Aufruf einen Stack iteriert. Zusätzlich zu der Verifikation mit diesen Datenstrukturen, definieren wir die Tiefensuch-Eigenschaft, um zu zeigen, dass der Algorithmus den Graphen in einer gültigen Reihenfolge traversiert.
Schlussendlich vergleichen wir den Verifikationsprozess sowohl für rekursive, als auch für nicht rekursive Tiefensuche, jeweils mit den vier genannten Datenstrukturen. Verglichen werden sie unter verschiedenen Aspekten, wie der Dauer des Verifikationsprozesses oder der Größe des Beweises.
Damit diskutiert diese Arbeit die Vor- und Nachteile der vier Datenstrukturen, während der Verifikation eines Graph-Algorithmus. Außerdem zeigt sie, dass die rekursive Implemetierung mit KeY einfacher zu verifizieren war als die nicht-rekursive. Außerdem geben wird sowohl eine allgemeine Definition der Tiefensuch-Eigenschaft einer Graph-Traversierung gegeben, als auch ein Satz von Regeln, um in KeY mit Summen umzugehen.
Abstract (englisch):
Graphs and graph-based algorithms are ubiquitous. With their omnipresence, it is important that these graph-algorithms work correctly. To ensure that those algorithms behave correctly, they can be formally verified. Deductive program verification is used, to show that a program fulfills a formal specification of its behavior for every valid input, which is a non-trivial task. Also, there is not only one single implementation of graphs. Graphs can be represented by a variety of data structures that all have their advantages and disadvantages in terms of e.g. runtime or memory-usage.
... mehr
It is unclear, where potential bottlenecks might occur during the verification of graph-algorithms. Throughout these data structures, there are differences with respect to their suitability for deductive program-verification of graph-algorithms. Knowing with which graph-representations graph-algorithms are easier to verify, provides an additional decision aid, when selecting an implementation.
In this thesis, we look at one specific algorithm: depth-first search. DFS is a simple algorithm for traversing graphs. Many graph algorithms are based on DFS. So, despite its simplicity, the verification of depth-first search is of interest. We specify and verify two different implementations of depth-first search. To do so, we use the formal specification language JML, to specify Java programs, and the KeY tool for deductive verification. We study each implementation with four different graph-representations. The considered graph data structures are the adjacency matrix, adjacency array and adjacency lists as well as a linked data structure using objects and pointers. As implementation of depth-first search, we use the recursive versions, using recursive method-calls, and the non-recursive version, iterating a loop instead of recursive calls. We show that the recursive version is verified for all four data structures, while the non-recursive version is only verified for the adjacency matrix version.
Additionally to the verification of DFS with different data structures, we define the depth-first property of a graph traversal, in order to prove that the algorithm traverses the graph in a valid order.
Finally, we compare the verification-process of recursive and non-recursive depth-first search, for all four representations. We compare them in terms of different aspects, like the time effort of the verification process or the size of the resulting proof.
In the end, this thesis discusses advantages and disadvantages of the four graph-representations, during the verification of a graph-algorithm. Additionally, we see how the recursive implementation of DFS can be easier to verify with KeY, than the non-recursive version. Furthermore, we give a general definition of the depth-first property of a graph traversal and a set of rules to handle bounded sums in KeY.
