Mutation in Linked Data Structures

Separation logic was developed as an extension to Hoare logic with the aim of simplifying pointer program proofs. A key feature of the logic is that it focuses the reasoning effort on only those parts of the heap that are relevant to a program - so called local reasoning. Underpinning this local reasoning are the

separating conjunction

and

separating implication

operators. Here we present an automated reasoning technique called

mutation

that provides guidance for separation logic proofs. Specifically, given two heap structures specified within separation logic, mutation attempts to construct an equivalence proof using a difference reduction strategy. Pivotal to this strategy is a generalised decomposition operator which is essential when matching heap structures. We show how mutation provides an effective strategy for proving the functional correctness of iterative and recursive programs within the context of weakest precondition analysis. Currently, mutation is implemented as a proof plan within our CORE program verification system. CORE combines results from shape analysis with our work on invariant generation and proof planning. We present our results for mutation within the context of the CORE system.