Verified rank-balanced trees using LiquidHaskell

Abstract

This thesis presents a comprehensive verification of the weak AVL tree, a variant of the classic AVL tree that allows for more flexibility in balancing operations. The study focuses on three critical aspects of the WAVL tree: termination, functional correctness, and amortized complexity analysis of its resource usage. Functional correctness is assessed by demonstrating, through LiquidHaskell, that the WAVL tree accurately implements its specified operations—insertions, deletions, and searches—while maintaining all weak AVL properties. An in-depth amortized complexity analysis is conducted to formally verify the WAVL tree's resource usage over sequences of operations, thereby confirming its efficiency and performance characteristics. This verification solidifies the WAVL tree as a robust data structure and contributes significantly to the field of data structures by detailing advanced verification techniques with LiquidHaskell that ensure reliability and efficiency.

Diese Arbeit präsentiert eine umfassende Überprüfung des WAVL-Baums (weak AVL), einer Variante des klassischen AVL-Baums, der mehr Flexibilität bei den Balancierungsoperationen ermöglicht. Die Studie konzentriert sich auf drei kritische Aspekte des WAVL-Baums: Terminierung, funktionale Korrektheit und amortisierte Komplexitätsanalyse seiner Ressourcennutzung. Die funktionale Korrektheit wird durch den Einsatz von LiquidHaskell bewertet, indem demonstriert wird, dass der WAVL-Baum seine Operationen, Einfügen und Löschen, korrekt implementiert und dabei alle Eigenschaften beibehält. Eine detaillierte amortisierte Komplexitätsanalyse wird durchgeführt, um den Ressourcenverbrauch des WAVL-Baums über eine Reihe von Operationen für die Ausbalancierung des Baums formal zu beweisen und somit seine Effizienz und Leistungsmerkmale zu bestätigen. Diese Überprüfung festigt nicht nur die Position des WAVL-Baums als robuste Datenstruktur, sondern trägt auch erheblich zum Bereich der Datenstrukturen bei, indem sie fortgeschrittene Verifikationstechniken mit LiquidHaskell detailiert darlegt, die Zuverlässigkeit und Effizienz gewährleisten.