Abstract
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.
The research reported in this paper is supported by EPSRC grant EP/F037597. Our thanks go to Gudmund Grov for his feedback and encouragement with this work.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Atkey, R.: Amortised resource analysis with separation logic. In: 19th European Symposium on Programming, pp. 85–103 (2010)
Berdine, J., Calcagno, C., O’Hearn, P.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115–137. Springer, Heidelberg (2006)
Berdine, J., Calcagno, C., O’Hearn, P.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52–68. Springer, Heidelberg (2005)
Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk, R., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 111–120. Springer, Heidelberg (1988)
Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-level Guidance for Mathematical Reasoning. Cambridge University Press, Cambridge (2005)
Burstall, R.M.: Some techniques for proving correctness of programs. In: Machine Intelligence, vol. 7, pp. 23–50. Edinburgh University Press, Edinburgh (1972)
Distefano, D., Parkinson, M.J.: jstar: towards practical verification for java. In: Proceedings of the 23rd ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications, OOPSLA 2008, pp. 213–226. ACM, New York (2008)
Dixon, L., Fleuriot, J.D.: IsaPlanner: A prototype proof planner in isabelle. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 279–283. Springer, Heidelberg (2003)
Ireland, A., Maclean, E., Grov, G.: Verification and synthesis of functional correctness of pointer programs. Research Memo HW-MACS-TR-0087, School of Mathematical and Computer Sciences, Heriot-Watt University (2011)
Maclean, E., Ireland, A., Grov, G.: The core system: Animation and functional correctness of pointer programs, Under review as a ASE-11 Tool Demonstration paper (2011)
Nguyen, H.H., David, C., Qin, S., Chin, W.N.: Automated verification of shape and size properties via separation logic. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 251–266. Springer, Heidelberg (2007)
Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
O’Hearn, P., Reynolds, J., Hongseok, Y.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Logic in Computer Science, pp. 55–74. IEEE Computer Society, Los Alamitos (2002)
Tuerk, T.: A formalisation of smallfoot in HOL. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 469–484. Springer, Heidelberg (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Maclean, E., Ireland, A. (2011). Mutation in Linked Data Structures. In: Qin, S., Qiu, Z. (eds) Formal Methods and Software Engineering. ICFEM 2011. Lecture Notes in Computer Science, vol 6991. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24559-6_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-24559-6_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24558-9
Online ISBN: 978-3-642-24559-6
eBook Packages: Computer ScienceComputer Science (R0)