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{W...
| Format: | Journal article |
|---|---|
| Published: |
Cambridge University Press
2001
|
| Subjects: |
| _version_ | 1797104125288120320 |
|---|---|
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-07T06:29:24Z |
| format | Journal article |
| id | oxford-uuid:f5754705-10ee-4fe0-b692-c16481d9be2b |
| institution | University of Oxford |
| last_indexed | 2024-03-07T06:29:24Z |
| publishDate | 2001 |
| publisher | Cambridge University Press |
| record_format | dspace |
| spelling | oxford-uuid:f5754705-10ee-4fe0-b692-c16481d9be2b2022-03-27T12:27:27ZFUNCTIONAL PEARL Unfolding pointer algorithmsJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:f5754705-10ee-4fe0-b692-c16481d9be2bComputing LaboratoryOxford University Research Archive - ValetCambridge University Press2001A 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. |
| spellingShingle | Computing Laboratory FUNCTIONAL PEARL Unfolding pointer algorithms |
| title | FUNCTIONAL PEARL
Unfolding pointer algorithms |
| title_full | FUNCTIONAL PEARL
Unfolding pointer algorithms |
| title_fullStr | FUNCTIONAL PEARL
Unfolding pointer algorithms |
| title_full_unstemmed | FUNCTIONAL PEARL
Unfolding pointer algorithms |
| title_short | FUNCTIONAL PEARL
Unfolding pointer algorithms |
| title_sort | functional pearl unfolding pointer algorithms |
| topic | Computing Laboratory |