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
verification of the Schorr–Waite marking algorithm, including Gries (1979, Morris
(1982) and Topor (1979). Bornat (2000) writes: “The Schorr–Waite algorithm is the
first 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öeller, 1993), in data refinement
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-defined 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öller (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.
FUNCTIONAL PEARL Unfolding pointer algorithms