Verification of tree-like data structures with iterators in Dafny

Abstract

Tree-like data structures are a common way to implement important data types that are pervasively used in many programming languages. Specifically selfbalancing binary search trees can guarantee logarithmic cost for the main operations, making them the implementation choice of many container libraries. In this work we give a specfication for sets, maps and multisets in the Dafny programming language. We also implement and verify in Dafny left-leaning red-black trees, a kind of self-balancing binary search tree, following the same methodology that we developed in our previous work. Lastly, we advance on the implementation and verification of iterators for binary search trees.

Las estructuras de datos arborescentes son una forma común de implementar tipos de datos importantes que se usan de forma generalizada en muchos lenguajes de programación. Concretamente, los árboles de búsqueda autoequilibrados pueden garantizar coste logarítmico para las operaciones principales, haciéndolos la implementación elegida de muchas bibliotecas de contenedores de datos. En este trabajo damos una especificación de conjuntos, mapas y multiconjuntos en el lenguaje de programación Dafny. También implementamos y verificamos en Dafny los árboles rojinegros inclinados a la izquierda, un tipo de árbol autoequilibrado, siguiendo la metodología que desarrollamos en trabajo previo. Finalmente, avanzamos en la implementación y verificación de los iteradores para árboles binarios de búsqueda.