Abstract
Hoare logic ([7]) is an important tool for formally proving correctness properties of programs. It takes advantage of modularity by treating program fragments in terms of provable specifications. However, heap programs tend to break this type of modular reasoning by permitting pointer aliasing. For instance, the specification that a program reverses one list does not imply that it leaves a second list alone. To achieve this disjointness property, it is necessary to establish disjointness conditions throughout the proof.
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
Calcagno, C., Gardner, P., Zarfaty, U.: Context Logic and tree update. In: POPL 2005, pp. 271–282 (2005)
Calcagno, C., Gardner, P., Zarfaty, U.: Local reasoning about data update. ENTCS 172, 133–175 (2007)
de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and Their Comparison. Cambridge University Press, Cambridge (1999)
Dinsdale-Young, T., Gardner, P., Wheelhouse, M.: Abstraction and refinement for local reasoning. In: Leavens, G.T., O’Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol. 6217, pp. 199–215. Springer, Heidelberg (2010)
Filipović, I., O’Hearn, P., Torp-Smith, N., Yang, H.: Blaming the client: on data refinement in the presence of pointers. Formal Aspects of Computing (2009)
Gardner, P.A., Smith, G.D., Wheelhouse, M.J., Zarfaty, U.D.: Local Hoare reasoning about DOM. In: PODS, pp. 261–270 (2008)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)
Hoare, C.A.R.: Proof of correctness of data representations. Acta Inf. 1(4), 271–281 (1972)
Mijajlović, I., Torp-Smith, N., O’Hearn, P.W.: Refinement and separation contexts. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 421–433. Springer, Heidelberg (2004)
Mitchell, J.C., Plotkin, G.D.: Abstract types have existential type. In: POPL, pp. 37–51 (1985)
O’Hearn, P.W., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, p. 1. Springer, Heidelberg (2001)
Parkinson, M.J., Bierman, G.M.: Separation logic and abstraction. In: POPL, pp. 247–258 (2005)
Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: IFIP Congress, pp. 513–523 (1983)
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
Dinsdale-Young, T., Gardner, P., Wheelhouse, M. (2011). Abstract Local Reasoning for Program Modules. In: Corradini, A., Klin, B., Cîrstea, C. (eds) Algebra and Coalgebra in Computer Science. CALCO 2011. Lecture Notes in Computer Science, vol 6859. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22944-2_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-22944-2_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22943-5
Online ISBN: 978-3-642-22944-2
eBook Packages: Computer ScienceComputer Science (R0)