Graph Types

13 years 8 months ago

Download www.daimi.au.dk

e data structures are abstractions of simple records and pointers. They impose a shape invariant, which is veriﬁed at compiletime and exploited to automatically generate code for buildings copying, comparing, and traversing values without loss of eﬃciency. 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 eﬃciently. We deﬁne regular languages of routing expressions to specify relative addresses of extra pointers in a canonical spanning tree. An eﬃcient algorithm for computing such addresses is developed. We employ a second order monadic logic to decide well-formedness of graph type speciﬁcations. 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

Real-time Traffic