Workshop on Specification and Verification of Component-Based Systems, Challenge Problem Track edition:7 location:Atlanta, GA, USA date:9-10 November 2008
Often, a module developer wishes to expose a graph of objects to client code, allowing client code to access the graph through any node directly, while maintaining hidden consistency conditions over the graph. In this note, we describe how to specify and verify such code using separation logic, using as an example a binary tree structure where each node keeps a count of its descendant nodes. The idea is to describe the tree structure as the separate conjunction of the focus node’s subtree and the focus node’s context. The description can be rewritten to use any other node as the focus node at any time. This enables an elegant modular proof of the tree implementation
on the one hand, and client code on the other hand.
We describe how we verified an example program using the
VeriFast program verifier prototype.