Graph Types

e data structures are abstractions of simple records and pointers. They impose a shape invariant, which is verified at compiletime and exploited to automatically generate code for buildings copying, comparing, and traversing values without loss of efficiency. However, such values are always tree shaped, which is a major obstacle to practical use. We propose a notion of graph types, which allow common shapes, such as doubly-linked lists or threaded trees, to be expressed concisely and efficiently. We define regular languages of routing expressions to specify relative addresses of extra pointers in a canonical spanning tree. An efficient algorithm for computing such addresses is developed. We employ a second order monadic logic to decide well-formedness of graph type specifications. This logic can also be used for automated reasoning about pointer structures. ∗ This paper will also be presented at POPL’93; references should cite the proceedings. † The author is supported by a f...

• Type: Conference
• Year: 1993
• Where: POPL
• Authors: Nils Klarlund, Michael I. Schwartzbach
• Keywords: Canonical Spanning Tree, Danish Research Council, Graph Type, POPL 1993, Programming Languages