Enforcing structural invariants using dynamic frames

The theory of dynamic frames is a promising approach to handle the so-called framing problem, that is, giving a precise characterizations of the locations in the heap that a procedure may modify. In this paper, we show that the machinery used for dynamic frames may be exploited even further. In part...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	Garbervetsky, Diego, Gorín, Daniel Alejandro
Publicado:	2011
Materias:	Abstract data types Dynamic frame Non-circular Non-trivial Programming language Structural invariants Theory of dynamics Algorithms Machinery Trees (mathematics)
Acceso en línea:	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v6605LNCS_n_p65_Garbervetsky http://hdl.handle.net/20.500.12110/paper_03029743_v6605LNCS_n_p65_Garbervetsky
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	paper:paper_03029743_v6605LNCS_n_p65_Garbervetsky
record_format	dspace
spelling	paper:paper_03029743_v6605LNCS_n_p65_Garbervetsky2023-06-08T15:28:39Z Enforcing structural invariants using dynamic frames Garbervetsky, Diego Gorín, Daniel Alejandro Abstract data types Dynamic frame Non-circular Non-trivial Programming language Structural invariants Theory of dynamics Algorithms Machinery Trees (mathematics) The theory of dynamic frames is a promising approach to handle the so-called framing problem, that is, giving a precise characterizations of the locations in the heap that a procedure may modify. In this paper, we show that the machinery used for dynamic frames may be exploited even further. In particular, we use it to check that implementations of abstract data types maintain certain structural invariants that are very hard to express with usual means, including being acyclic (like non-circular linked lists and trees) and having a unique path between nodes (like in a tree). The idea is that regions in this formalism over-approximate the set of reachable objects. We can then maintain this structural invariants by including special preconditions in assignments, of the kind that can be verified by state-of-the-art SMT-based tools. To test this approach we modified the verifier for the Dafny programming language in a suitable way and were able to enforce these invariants in non-trivial examples. © 2011 Springer-Verlag. Fil:Garbervetsky, D. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Gorín, D. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2011 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v6605LNCS_n_p65_Garbervetsky http://hdl.handle.net/20.500.12110/paper_03029743_v6605LNCS_n_p65_Garbervetsky
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-134
collection	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic	Abstract data types Dynamic frame Non-circular Non-trivial Programming language Structural invariants Theory of dynamics Algorithms Machinery Trees (mathematics)
spellingShingle	Abstract data types Dynamic frame Non-circular Non-trivial Programming language Structural invariants Theory of dynamics Algorithms Machinery Trees (mathematics) Garbervetsky, Diego Gorín, Daniel Alejandro Enforcing structural invariants using dynamic frames
topic_facet	Abstract data types Dynamic frame Non-circular Non-trivial Programming language Structural invariants Theory of dynamics Algorithms Machinery Trees (mathematics)
description	The theory of dynamic frames is a promising approach to handle the so-called framing problem, that is, giving a precise characterizations of the locations in the heap that a procedure may modify. In this paper, we show that the machinery used for dynamic frames may be exploited even further. In particular, we use it to check that implementations of abstract data types maintain certain structural invariants that are very hard to express with usual means, including being acyclic (like non-circular linked lists and trees) and having a unique path between nodes (like in a tree). The idea is that regions in this formalism over-approximate the set of reachable objects. We can then maintain this structural invariants by including special preconditions in assignments, of the kind that can be verified by state-of-the-art SMT-based tools. To test this approach we modified the verifier for the Dafny programming language in a suitable way and were able to enforce these invariants in non-trivial examples. © 2011 Springer-Verlag.
author	Garbervetsky, Diego Gorín, Daniel Alejandro
author_facet	Garbervetsky, Diego Gorín, Daniel Alejandro
author_sort	Garbervetsky, Diego
title	Enforcing structural invariants using dynamic frames
title_short	Enforcing structural invariants using dynamic frames
title_full	Enforcing structural invariants using dynamic frames
title_fullStr	Enforcing structural invariants using dynamic frames
title_full_unstemmed	Enforcing structural invariants using dynamic frames
title_sort	enforcing structural invariants using dynamic frames
publishDate	2011
url	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v6605LNCS_n_p65_Garbervetsky http://hdl.handle.net/20.500.12110/paper_03029743_v6605LNCS_n_p65_Garbervetsky
work_keys_str_mv	AT garbervetskydiego enforcingstructuralinvariantsusingdynamicframes AT gorindanielalejandro enforcingstructuralinvariantsusingdynamicframes
_version_	1768545925924388864

Enforcing structural invariants using dynamic frames

Ejemplares similares