FUNCTIONAL PEARL Unfolding pointer algorithms

A fair amount has been written on the subject of reasoning about pointer algorithms. There was a peak about 1980 when everyone seemed to be tackling the formal verication of the Schorr{Waite marking algorithm, including Gries (1979, Morris (1982) and Topor (1979). Bornat (2000) writes: \The Schorr{Waite algorithm is the rst mountain that any formalism for pointer aliasing should climb". Then it went more or less quiet for a while, but in the last few years there has been a resurgence of interest, driven by new ideas in relational algebras (M¨oeller, 1993), in data renement Butler (1999), in type theory (Hofmann, 2000; Walker and Morrisett, 2000), in novel kinds of assertion (Reynolds, 2000), and by the demands of mechanised reasoning (Bornat, 2000). Most approaches end up being based in the Floyd{Dijkstra{Hoare tradition with loops and invariant assertions. To be sure, when dealing with any recursively-dened linked structure some declarative notation has to be brought in to specify the problem, but no one to my knowledge has advocated a purely functional approach throughout. Mason (1988) comes close, but his Lisp expressions can be very impure. M¨oller (1999) also exploits an algebraic approach, and the structure of his paper has much in common with what follows. This pearl explores the possibility of a simple functional approach to pointer manipulation algorithms