Blázquez Saborido, JorgeMontenegro Montes, ManuelSegura Díaz, Clara María2023-06-222023-06-222023-082352-221610.1016/j.jlamp.2023.100875https://hdl.handle.net/20.500.14352/72274We 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.engAtribución-NoComercial-SinDerivadas 3.0 Españahttps://creativecommons.org/licenses/by-nc-nd/3.0/es/journal articlehttps://www.elsevier.com/locate/jlampopen access004.43004.89Program verificationData structuresAbstract data typesIteratorsDafnyVerificación de programasEstructuras de datosTipos abstractos de datos Iteradores DafnyLenguajes de programaciónSoftwareLógica simbólica y matemática (Matemáticas)1203.23 Lenguajes de Programación3304.16 Diseño Lógico1102.14 Lógica Simbólica