Tech Reports Home Contact
Technical Report Series
Submit Report
Browse Reports
Information for Authors
Contact Details

Technical Report HW-MACS-TR-0090

TitleMutation in Linked Data Structures
AuthorsEwen Maclean, Andrew Ireland
AbstractWe describe a technique, which we call "mutation" for decomposing and matching arbitrary linked data structures. This work is inspired by problems encountered when proving functional properties about programs specified using Separation Logic. In general these programs manipulate the heap, and use linked structures to encapsulate data. In Separation logic proofs which take a weakest precondition approach, the Hoare style rules for program constructs have been extended to account for pointer manipulation. This brings a pattern of reasoning where linked data structures must be decomposed in order to complete proofs, and then "mutated" so that hypotheses can apply. We introduce the notion of "Most General Decomposition" and "Compound Mutation Analysis", which heuristically determine whether any two arbitrary heaps involving linked data-structures can be matched. We demonstrate how this applies both to weakest-precondition style proofs, and forward style proofs such as those performed in Smallfoot, HolFoot and JStar.


Email Technical Report's Administrator
|MACS Home| Top of the Page

Department of Computer Science, Heriot-Watt University, Riccarton, Edinburgh, EH14 4AS, +44 (0) 131 4514152

Last Updated: 02 September 2003 Copyright Heriot-Watt University, Disclaimer