In this thesis, we use the interactive theorem prover Isabelle/HOL to verify an imperative implementation of the classical B-tree data structure. The implementation supports set membership and insertion queries with efficient binary search for intra-node navigation. This is accomplished by first specifying the structure abstractly in the functional modeling language HOL and proving functional correctness. Using manual refinement, we derive an imperative implementation in Imperative/HOL. We show the validity of this refinement using the separation logic utilities from the Isabelle Refinement Framework. The code can be exported to the programming languages SML and Scala. We examine the runtime of all operations indirectly by reproducing results of the logarithmic relationship between height and the number of nodes. Considering development time and lines of code, our approach compares well to other approaches at mechanized verifications of the B-tree data structure.     «

In this thesis, we use the interactive theorem prover Isabelle/HOL to verify an imperative implementation of the classical B-tree data structure. The implementation supports set membership and insertion queries with efficient binary search for intra-node navigation. This is accomplished by first specifying the structure abstractly in the functional modeling language HOL and proving functional correctness. Using manual refinement, we derive an imperative implementation in Imperative/HOL....     »

In dieser Arbeit wird mithilfe des interaktiven Theorembeweisers Isabelle/HOL eine imperative Version der klassischen B-Baum Datenstruktur verifiziert. Die Implementierung unterstützt Element- und Einfügeoperationen mit effizienter binärerer Suche für knoteninterne Navigation. Das Ergebnis wurde erzielt, indem die Struktur zuerst abstrakt in der Modellierungssprache HOL spezifiziert wurde, in der funktionale Korrektheit gezeigt werden konnte. Mithilfe von Verfeinerung wurde davon eine imperative Implementierung in Imperative/HOL abgeleitet. Mithilfe den Werkzeugen für Separationslogik des Isabelle Verfeinerungs Frameworks zeigen wir, dass die Verfeinerung gültig ist. Der Programmcode kann in die Sprachen SML und Scala exportiert werden. Wir untersuche zudem indirekt die Laufzeit der Operationen, indem wir klassische Ergebnisse über die logarithmische Beziehung zwischen Höhe und Anzahl Knoten reproduzieren. In Hinsicht auf Entwicklungszeit und Zeilen Programmcode liefert unser Ansatz gute Ergebnisse im Vergleich zu anderen Arbeiten zur maschinellen Verifikationen der B-Baum Datenstruktur.     «

In dieser Arbeit wird mithilfe des interaktiven Theorembeweisers Isabelle/HOL eine imperative Version der klassischen B-Baum Datenstruktur verifiziert. Die Implementierung unterstützt Element- und Einfügeoperationen mit effizienter binärerer Suche für knoteninterne Navigation. Das Ergebnis wurde erzielt, indem die Struktur zuerst abstrakt in der Modellierungssprache HOL spezifiziert wurde, in der funktionale Korrektheit gezeigt werden konnte. Mithilfe von Verfeinerung wurde davon eine imperati...     »