Enforcing structural invariants using dynamic frames

Mostrar todas las versiones(3)

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, D., Gorín, D., Neisen, A.
Formato: Artículo publishedVersion
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:http://hdl.handle.net/20.500.12110/paper_03029743_v6605LNCS_n_p65_Garbervetsky
https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=artiaex&d=paper_03029743_v6605LNCS_n_p65_Garbervetsky_oai
Aporte de:
Repositorio Digital de la Universidad de Buenos Aires (UBA) de Universidad de Buenos Aires
id I28-R145-paper_03029743_v6605LNCS_n_p65_Garbervetsky_oai
record_format dspace
spelling I28-R145-paper_03029743_v6605LNCS_n_p65_Garbervetsky_oai2024-08-16 Garbervetsky, D. Gorín, D. Neisen, A. 2011 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. application/pdf http://hdl.handle.net/20.500.12110/paper_03029743_v6605LNCS_n_p65_Garbervetsky info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar Lect. Notes Comput. Sci. 2011;6605 LNCS:65-80 Abstract data types Dynamic frame Non-circular Non-trivial Programming language Structural invariants Theory of dynamics Algorithms Machinery Trees (mathematics) Enforcing structural invariants using dynamic frames info:eu-repo/semantics/article info:ar-repo/semantics/artículo info:eu-repo/semantics/publishedVersion https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=artiaex&d=paper_03029743_v6605LNCS_n_p65_Garbervetsky_oai
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-145
collection Repositorio Digital de la Universidad de Buenos Aires (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, D.
Gorín, D.
Neisen, A.
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.
format Artículo
Artículo
publishedVersion
author Garbervetsky, D.
Gorín, D.
Neisen, A.
author_facet Garbervetsky, D.
Gorín, D.
Neisen, A.
author_sort Garbervetsky, D.
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 http://hdl.handle.net/20.500.12110/paper_03029743_v6605LNCS_n_p65_Garbervetsky
https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=artiaex&d=paper_03029743_v6605LNCS_n_p65_Garbervetsky_oai
work_keys_str_mv AT garbervetskyd enforcingstructuralinvariantsusingdynamicframes
AT gorind enforcingstructuralinvariantsusingdynamicframes
AT neisena enforcingstructuralinvariantsusingdynamicframes
_version_ 1809356905655566336

Ejemplares similares