Sciweavers

Share
ECOOP
2009
Springer

Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic

13 years 19 days ago
Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic
The dynamic frames approach has proven to be a powerful formalism for specifying and verifying object-oriented programs. However, it requires writing and checking many frame annotations. In this paper, we propose a variant of the dynamic frames approach that eliminates the need to explicitly write and check frame annotations. Reminiscent of separation logic's frame rule, programmers write access assertions inside pre- and postconditions instead of writing frame annotations. From the precondition, one can then infer an upper bound on the set of locations writable or readable by the corresponding method. We implemented our approach in a tool, and used it to automatically verify several challenging programs, including subject-observer, iterator and linked list.
Jan Smans, Bart Jacobs 0002, Frank Piessens
Added 22 Nov 2009
Updated 22 Nov 2009
Type Conference
Year 2009
Where ECOOP
Authors Jan Smans, Bart Jacobs 0002, Frank Piessens
Comments (0)
books