RT Journal Article
T1 Verification of mutable linear data structures and iterator-based algorithms in Dafny.
T2 Verificación de estructuras de datos lineales y algoritmos basado s en iteradores en Dafny.
A1 Blázquez Saborido, Jorge
A1 Montenegro Montes, Manuel
A1 Segura Díaz, Clara María
AB We address the verification of mutable, heap-allocated abstract data types (ADTs) in Dafny, and their traversal via iterators. For this purpose, we devise a verification methodology that makes it possible to implement ADTs based on already existing ones, while maintaining proper encapsulation. Then, we apply this methodology to the specification and implementation of linear collections such as stacks, queues, deques, and lists with iterators. The approach introduced in this paper allows one to progressively refine some aspects of the specification such as iterator invalidation, so that clients of the library can reason about how structural changes to a list affect existing iterators. Finally, we extend our methodology to the verification of client code (i.e., code that makes use of the implemented ADTs) and identify the boilerplate conditions common to all methods that receive and manipulate ADTs.
PB Elsevier
SN 2352-2216
YR 2023
FD 2023-08
LK https://hdl.handle.net/20.500.14352/72274
UL https://hdl.handle.net/20.500.14352/72274
LA eng
NO Ministerio de Economía y Competitividad
NO Ministerio de Ciencia e Innovación
NO Comunidad de Madrid
DS Docta Complutense
RD 15 jun 2025