Abstract Local reasoning, separation and aliasing

Structures built by pointer aliasing, such as DAGs and graphs, are notoriously tricky to deal with. The mechanisms of separation logic can deal with these structures, but so far this has been done by the maintenance of a global invariant. Specifications and proofs which use local reasoning, and which may point the way to a structured programming for pointers, are discussed. An idiom for inclusion sharing, where one structure is included in another, is presented. A notion of ‘partial graphs ’ – graphs with dangling pointers – is used to facilitate proof.