Enforcing structural invariants using dynamic frames

En:

Lect. Notes Comput. Sci. 2011;6605 LNCS:65-80

Fecha:

2011

Formato:

application/pdf

Tipo de documento:

info:eu-repo/semantics/article
info:ar-repo/semantics/artículo
info:eu-repo/semantics/publishedVersion

Descriptores:

Abstract data types -  Dynamic frame -  Non-circular -  Non-trivial -  Programming language -  Structural invariants -  Theory of dynamics -  Algorithms -  Machinery

Descripción:

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.

Identificador(es):

http://hdl.handle.net/20.500.12110/paper_03029743_v6605LNCS_n_p65_Garbervetsky

Derechos:

info:eu-repo/semantics/openAccess
http://creativecommons.org/licenses/by/2.5/ar