2026-06-08T12:22:34Zhttps://docta.ucm.es/rest/oai/requestoai:docta.ucm.es:20.500.14352/931862025-03-18T13:28:31Zcom_20.500.14352_14col_20.500.14352_15
Docta Complutense
author
Blázquez, Jorge
author
Montenegro Montes, Manuel
author
Segura Díaz, Clara María
2024-01-15T16:46:08Z
2024-01-15T16:46:08Z
2021-09-22
https://hdl.handle.net/20.500.14352/93186
https://hdl.handle.net/11705/PROLE/2021/015
https://sistedes2021.spilab.es/prole/
We address the verification of mutable, heap-allocated abstract data types (ADTs) in Dafny. In particular, we devise a generic verification methodology and apply it to the specification and implementation of linear collections such as stacks,
queues, deques, and lists with iterators. The layered approach presented in this paper allows us to progressively refine some aspects of the specification, such as iterator invalidation. We also introduce a stratified view of the footprint of an
instance (i.e. the set of memory locations owned by that instance), and identify the boilerplate conditions common to all operations of an ADT. We also show the usage of the resulting implementations by means of verified examples.
eng
Attribution-NonCommercial-NoDerivatives 4.0 International
Verification of mutable data structures in Dafny: methodological aspects
conference paper
UGFyYSBxdWUgZWwgcmVwb3NpdG9yaW8gaW5zdGl0dWNpb25hbCBkZSBsYSBVbml2ZXJzaWRhZCBkZSBNYWRyaWQgcHVlZGEgYWxtYWNlbmFyIHkgZGlzdHJpYnVpciBlbCBvYmpldG8gZGlnaXRhbCBkZXBvc2l0YWRvLCBlcyBuZWNlc2FyaW8gcXVlIGxhIHBlcnNvbmEgcXVlIGhhZ2EgZWwgZGVww7NzaXRvIGxlYSB5IGFjZXB0ZSBsYXMgY29uZGljaW9uZXMgZXN0YWJsZWNpZGFzIGVuIGVzdGEgbGljZW5jaWE6CuKAoiBBY2VwdGFuZG8gZXN0YSBsaWNlbmNpYSwgdXN0ZWQgY29tbyBhdXRvci9yZXMgeS9vIHByb3BpZXRhcmlvL3MgZGUgbG9zIGRlcmVjaG9zIGRlIHByb3BpZWRhZCBpbnRlbGVjdHVhbCwgb3RvcmdhIGFsIHJlcG9zaXRvcmlvIGRlIGxhIFVuaXZlcnNpZGFkIENvbXBsdXRlbnNlIGRlIE1hZHJpZCBlbCBkZXJlY2hvIG5vIGV4Y2x1c2l2byBkZSByZXByb2R1Y2Npw7NuIHkgZGlzdHJpYnVjacOzbiBkZSBzdSBvYnJhIGVuIGN1YWxxdWllciBmb3JtYXRvIHkgbWVkaW8uCuKAoiBFbCBkZXBvc2l0YW50ZSwgZW4gY2FzbyBkZSB1bmEgb2JyYSBjb24gbcOhcyBkZSB1biBhdXRvciwgZ2FyYW50aXphIHF1ZSBsbyBoYWNlIHJlc3BvbnNhYmxlbWVudGUgZW4gbm9tYnJlIHkgY29uIGNvbnNlbnRpbWllbnRvIGRlIGxvcyBkZW3DoXMgYXV0b3Jlcy4K4oCiIEFjZXB0YSBxdWUgZWwgcmVwb3NpdG9yaW8gZGUgbGEgVW5pdmVyc2lkYWQgQ29tcGx1dGVuc2UgZGUgTWFkcmlkIHB1ZWRhIGNvbnNlcnZhciBtw6FzIGRlIHVuYSBjb3BpYSBkZSBlc3RlIGRvY3VtZW50byB5LCBzaW4gYWx0ZXJhciBzdSBjb250ZW5pZG8sIGNvbnZlcnRpcmxvIGEgY3VhbHF1aWVyIGZvcm1hdG8gZGUgZmljaGVybywgbWVkaW8gbyBzb3BvcnRlLCBwYXJhIHByb3DDs3NpdG9zIGRlIHNlZ3VyaWRhZCB5IHByZXNlcnZhY2nDs24uCuKAoiBEZWNsYXJhIHF1ZSBlbCBkb2N1bWVudG8gZXMgdW4gdHJhYmFqbyBvcmlnaW5hbCBzdXlvIHkgcXVlIGN1ZW50YSBjb24gbGEgcG9zdGVzdGFkIHBhcmEgb3RvcmdhciBsb3MgZGVyZWNob3MgY29udGVuaWRvcyBlbiBlc3RhIGxpY2VuY2lhLiBUYW1iacOpbiBkZWNsYXJhIHF1ZSBzdSBkb2N1bWVudG8gbm8gaW5mcmluZ2UgbG8gZXN0YWJsZWNpZG8gZW4gbGEgdmlnZW50ZSBsZWdpc2xhY2nDs24gZGUgcHJvcGllZGFkIGludGVsZWN0dWFsLgrigKIgU2kgZWwgZG9jdW1lbnRvIGNvbnRpZW5lIG1hdGVyaWFsZXMgZGUgbG9zIGN1YWxlcyBubyB0aWVuZSBsb3MgZGVyZWNob3MgZGUgYXV0b3IsIGRlY2xhcmEgcXVlIGhhIG9idGVuaWRvIGVsIHBlcm1pc28gc2luIHJlc3RyaWNjacOzbiBkZWwgcHJvcGlldGFyaW8gcGFyYSBvdG9yZ2FyIGEgbGEgVW5pdmVyc2lkYWQgQ29tcGx1dGVuc2UgZGUgTWFkcmlkIGxvcyBkZXJlY2hvcyByZXF1ZXJpZG9zIHBvciBlc3RhIGxpY2VuY2lhLCB5IHF1ZSBlc2UgbWF0ZXJpYWwsIGN1eW9zIGRlcmVjaG9zIHNvbiBkZSB0ZXJjZXJvcywgZXN0w6EgY2xhcmFtZW50ZSBpZGVudGlmaWNhZG8geSByZWNvbm9jaWRvIGRlbnRybyBkZWwgY2NvbnRlbmlkbyBkZWwgZG9jdW1lbnRvLgrigKIgU2kgZWwgZG9jdW1lbnRvIHNlIGJhc2EgZW4gdW5hIG9icmEgcXVlIGhhIHNpZG8gcGF0cm9jaW5hZGEgbyBhcG95YWRhIHBvciB1bmEgYWdlbmNpYSB1IG9yZ2FuaXphY2nDs24gZGlmZXJlbnRlIGRlIGxhIFVuaXZlcnNpZGFkIENvbXBsdXRlbnNlIGRlIE1hZHJpZCwgdXN0ZWQgZGVjbGFyYSBxdWUgaGEgY3VtcGxpZG8gY29uIGxhcyBvYmxpZ2FjaW9uZXMgcmVxdWVyaWRhcyBwb3IgZXN0ZSBjb250cmF0byBvIGFjdWVyZG8uCuKAoiBMYSBVbml2ZXJzaWRhZCBDb21wbHV0ZW5zZSBkZSBNYWRyaWQgaWRlbnRpZmljYXLDoSBjbGFyYW1lbnRlIHN1L3Mgbm9tYnJlL3MgY29tbyBlbC9sb3MgYXV0b3IvZXMgbyBwcm9waWV0YXJpby9zIGRlIGxvcyBkZXJlY2hvcyBkZWwgZG9jdW1lbnRvLCB5IG5vIGhhcsOhIG5pbmd1bmEgYWx0ZXJhY2nDs24gZGUgc3UgZG9jdW1lbnRvIGRpZmVyZW50ZSBhIGxhcyBwZXJtaXRpZGFzIGVuIGVzdGEgbGljZW5jaWEuCuKAoiBUcmFiYWpvcyBkZXBvc2l0YWRvcyBwb3Igc3UgcHJvcGlvIGF1dG9yOiBhbCBhdXRvLWFyY2hpdmFyIGVzdGEgY29sZWNjacOzbiBkZSBmaWNoZXJvcyB5IG1ldGFkYXRvcyBiaWJsaW9ncsOhZmljb3MgYXNvY2lhZG9zLCBvdHJvZ28sIGFsIHJlcG9zaXRvcmlvIGluc3RpdHVjaW9uYWwgZGUgbGEgVW5pdmVyc2lkYWQgQ29tcGx1dGVuc2UgZGUgTWFkcmlkIGVsIGRlcmVjaG8gcGFyYSBhbG1hY2VuYXJsb3MgeSBkaXN0cmlidWlybG9zLiBEZWNsYXJvIHF1ZSBlc3RlIG1hdGVyaWFsIGVzIGRlIG1pIHByb3BpZWRhZCBpbnRlbGVjdHVhbCB5IHF1ZSBlbCByZXBvc2l0b3JpbyBpbnN0aXR1dGljaW9uYWwgZGUgbGEgVW5pdmVyc2lkYWQgQ29tcGx1dGVuc2UgZGUgTWFkcmlkLCBubyBhc3VtZSByZXNwb25zYWJpbGlkYWQgYWxndW5hIGVuIGNhc28gZGUgcXVlIHNlIHByb2R1emNhIHVuYSB2aW9sYWNpw7NuIGRlIGRlcmVjaG9zIGRlIHByb3BpZWRhZCBhbCBkaXN0cmlidWlyIGVzdG9zIGZpY2hlcm9zIG8gbWV0YWRhdG9zLgrigKIgVHJhYmFqb3MgZGVzcG9zaXRhZG9zIHBvciBvdHJvcyBxdWUgbm8gc2VhbiBzdSBhdXRvcjpkZWNsYXJvIHF1ZSBsb3MgbWV0YWRhdG9zIGJpYmxpb2dyw6FmaWNvcyBxdWUgZXN0b3kgYXJjaGl2YW5kbyBlbiBlbCByZXBvc3RvcmlvIGluc3RpdHVjaW9uYWwgZGUgbGEgVW5pdmVyc2lhZCBDb21wbHV0ZW5zZSBkZSBNYWRyaWQsIHNvbiBkZSBkb21pbmlvIHDDumJsaWNvLiBTaSBubyBmdWVzZSBlbCBjYXNvLCBhY2VwdG8gcGxlbmEgcmVzcG9uc2FiaWxpZGFkIHBvciBjdWFscXVpZXIgaW5mcmFjY2nDs24gZGUgZGVyZWNob3MgZGUgYXR1b3IgcXVlIGNvbmxsZXZlIGxhIGRpc3RyaWJ1Y2nDs24gZGUgZXN0b3MgZmljaGVyb3MgbyBtZXRhZGF0b3MuCuKAoiBQb3IgdGFudG8sIHRvZG9zIGxvcyBtZXRhZGF0b3MgcHVibGljYWRvcyBlbiBlbCByZXBvc2l0b3JpbyBpbnN0aXR1Y2lvbmFsIGRlIGxhIFVuaXZlcnNpZGFkIENvbXBsdXRlbnNlIGRlIE1hZHJpZCwgZXN0w6FuIGRpc3BvbmlibGVzIGNvbiBsYSBsaWNlbmNpYSBDcmVhdGl2ZSBDb21tb25zIENDMCAxLjAgVW5pdmVyc2FsIE9mcmVjaW1pZW50byBhbCBEb21pbmlvIFDDumJsaWNvIChDQzAgMS4wKS4gRXN0YSBsaWNlbmNpYSBwZXJtaXRlIGNvcGlhciwgbW9kaWZpY2FyLCBkaXN0cmlidWlyLCByZXV0aWxpemFyIHkgY29tcGFydGlyIHDDumJsaWNhIHkgbGlicmVtZW50ZSBsb3MgbWV0YWRhdG9zIChpbmNsdXllbmRvIHN1IHVzbyBjb21lcmNpYWwpLCBzaW4gdGVuZXIgcXVlIHBlZGlyIHBlcm1pc28uIFNpIHRlcmNlcmFzIHBhcnRlcyB1c2FuIGVzdG9zIG1ldGFkYXRvcywgZGViZW4gaGFjZXIgdW4gcmVjb25vY2ltaWVudG8geSB1bmEgYXRyaWJ1Y2Npw7NuIGEgbGFzIGZ1ZW50ZXMgZGUgbG9zIG1pc21vcy4gTGEgcmV1dGlsaXphY2nDs24gZGUgZXN0b3MgbWV0YWRhdG9zIHRhbWJpw6luIGVzIGxpYnJlLCB0YWwgeSBjb21vIGVzdGFibGVjZSBsYSBsaWNlbmNpYSBkZSB1c28gQ0MwLgo=
URL
https://docta.ucm.es/bitstreams/073d8816-3d59-43be-8d2a-de36bc2ccac7/download
File
MD5
640a64f876619a42bb46d7744e82bad3
272738
application/pdf
11705-PROLE-2021-015.pdf
URL
https://docta.ucm.es/bitstreams/0a38df84-111f-45ac-89dc-1a4abd6c0433/download
File
MD5
0c0205917b96e41c106084d0fc0b0dc5
37512
text/plain
11705-PROLE-2021-015.pdf.txt