Verification of Red-Black Trees in KeY - A Case Study in Deductive Java Verification

Abstract

Während das ausführliche Testen von Software das Auftreten von Fehlern unwahrscheinlicher macht, kann mit formaler Verifikation durch Beweise garantiert werden, dass sich ein Programm für sämtliche Eingaben korrekt verhält. Besonders für tausendfach verwendete Grundelemente wie die Datenstrukturen und Algorithmen einer Standardbibliothek ist eine formale Verifikation daher erstrebenswert. In dieser Fallstudie spezifizieren und verifizieren wir eine Java-Implementierung von Rot-Schwarz-Bäumen mit KeY. KeY ist ein Tool zur formalen Verifikation von Java-Programmen, und verwendet dabei Dynamic Frames für Aussagen über Speicherbereiche, also das Framing. Rot-Schwarz-Bäume sind eine beliebte Datenstruktur für das effiziente Speichern und Auslesen von Elementen und sind zum Beispiel in der Klasse java.util.TreeMap der Java Class Library umgesetzt. In beiden Bereichen existieren verschiedenste Fallstudien – die in KeY betrachten jedoch kaum Baumstrukturen und existierende Rot-Schwarz-Baum-Verifizierungen gehen auf andere Weise als KeY mit Framing um. In dieser Arbeit kommen wir zu dem Schluss, dass die Verifikation von Baumstrukturen mit Dynamic Frames möglich ist, jedoch im Vergleich zu anderen Ansätzen viel zusätzlichen Aufwand mit sich bringt. Darüber hinaus erkunden wir generelle Stärken und Schwächen von KeY und machen einige Vorschläge zur Verbesserung der Benutzbarkeit. Außerdem testen wir mit JML Scripts und Proof Caching neue Methoden zur Beweis-Automatisierung und -Persistierung.