Verification of tree-like data structures with iterators in Dafny
| Autor: | Blázquez Saborido, Jorge |
|---|---|
| Přispěvatelé: | Segura Díaz, Clara María, Montenegro Montes, Manuel |
| Jazyk: | angličtina |
| Rok vydání: | 2022 |
| Předmět: | |
| Zdroj: | E-Prints Complutense. Archivo Institucional de la UCM instname |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|