This paper aims to provide a better formalism for describing properties of linked data structures (e.g., lists, trees, graphs), as well as the intermediate states that arise when such structures are destructively updated. The paper defines a new logic that is suitable for these purposes (called L_r, for ``logic of reachability expressions''). We show that L<sub>r</sub> is decidable, and explain how L<sub>r</sub> relates to two previously defined structure-description formalisms (``path matrices'' and ``static shape graphs'') by showing how an arbitrary shape descriptor from each of these formalisms can be translated into an L_r formula.

(Click here to access the paper: PostScript, PDF.)