RT Generic
T1 Verification of tree-like data structures with iterators in Dafny
T2 Verificación de estructuras de datos arborescentes con iteradores en Dafny
A1 Blázquez Saborido, Jorge
AB 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.
AB 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.
YR 2022
FD 2022-09-09
LK https://hdl.handle.net/20.500.14352/73992
UL https://hdl.handle.net/20.500.14352/73992
LA eng
NO Trabajo de Fin de Master en Métodos Formales en Ingeniería Informática, Facultad de Informática UCM, Departamento de Sistemas Informáticos y Computación, Curso 2021/2022
DS Docta Complutense
RD 10 abr 2025