Specifying pointer structures by graph reduction

Abstract

Graph reduction specifications (GRSs) are a powerful new method for specifying classes of pointer data structures (shapes). They cover important shapes, like various forms of balanced trees, that cannot be handled by existing methods. This paper formally defines GRSs as graph reduction systems with a signature restriction and an accepting graph. We are mainly interested in PGRSs - polynomials-terminating GRSs whose graph languages are closed under reduction and have a polynomial membership test. We investigate the power of the PGRS framework by presenting example specifications and by considering its language closure properties: PGRS languages are closed under intersection; not closed under union (unless we drop the closedness restriction and exclude languages with the empty graph); and not closed under complement. Our practical investigation presents example PGRSs including cyclic lists, trees, balanced trees and red-black trees. In each case we try to make the PGRS as simple as possible where simpler means fewer rules, simpler termination and closure proofs and fewer non-terminals. We show how to prove the correctness of a PGRS and give methods for demonstrating that a given shape cannot be specified by a PGRS with certain simplicity properties. © Springer-Verlag 2004.