Verification of Scapegoat Trees Using Dafny

Self-balancing binary search trees are essential in Computer Science for their versatility and efficient management of ordered data. While a clear definition might exist for a specific kind of balanced tree, multiple implementations can exist. This diversity highlights the critical importance of verifying the correctness of a specific implementation. With this perspective, this paper shifts focus to the scapegoat tree, a type of self-balancing tree, prized for its operational simplicity. Utilizing the formal verification tool, Dafny, we undertake a rigorous examination of a scapegoat tree implementation. Through Dafny’s powerful specification and verification techniques, we prove the correctness of its core operations within our chosen implementation. We also summarized our user experience with Dafny, presenting several techniques that can enhance the efficiency of the proof process.