Graph Types

13 years 1 months ago
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...
Nils Klarlund, Michael I. Schwartzbach
Added 10 Aug 2010
Updated 10 Aug 2010
Type Conference
Year 1993
Where POPL
Authors Nils Klarlund, Michael I. Schwartzbach
Comments (0)