Abstract
O’Hearn, Reynolds and Yang introduced Separation Logic to provide modular reasoning about simple, mutable data structures in memory. They were able to construct small specifications of programs, by reasoning about the local parts of memory accessed by programs. Gardner, Calcagno and Zarfaty generalised this work, introducing Context Logic to reason about more complex data structures. In particular, they developed a formal, compositional specification of the Document Object Model, a W3C XML update library. Whilst keeping to the spirit of local reasoning, they were not able to retain small specifications. We introduce Segment Logic, which provides a more fine-grained analysis of the tree structure and yields small specifications. As well as being aesthetically pleasing, small specifications are important for reasoning about concurrent tree update.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Berdine, J., Calcagno, C., O’Hearn, P.W.: 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)
Calcagno, C., Dinsdale-Young, T., Gardner, P.: Adjunct elimination in context logic for trees. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 255–270. Springer, Heidelberg (2007)
Calcagno, C., Gardner, P., Zarfaty, U.: Context logic and tree update. In: POPL, vol. 40, ACM, New York (2005)
Cardelli, L., Gordon, A.D.: Ambient logic. Mathematical Structures in Computer Science (in press, 2006)
Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing 13 (2002)
Gardner, P., Smith, G., Wheelhouse, M., Zarfaty, U.: Local Hoare reasoning about DOM. In: PODS, vol. 27, ACM, New York (2008)
Gardner, P., Wheelhouse, M.: Small specifications for tree update (extended version) (2009), http://www.doc.ic.ac.uk/~mjw03/PersonalWebpage/pdfs/moveFull.pdf
Gardner, P., Zarfaty, U.: Reasoning about high-level tree update and its low-level implementation. Technical Report DTR09-9, Imperial College (2009)
Hosoya, H., Pierce, B.C.: Xduce: A statically typed XML processing language. In: TOIT 2003, vol. 3, ACM, New York (2003)
Ishtiaq, S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: POPL 2001, vol. 36, ACM, New York (2001)
Milner, R.: Pi-nets: A graphical form of π-calculus. In: Sannella, D. (ed.) ESOP 1994. LNCS, vol. 788, Springer, Heidelberg (1994)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes I & II. Information and Computation 100 (1992)
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. 15. Springer, Heidelberg (2001)
O’Hearn, P.W.: Resources, concurrency and local reasoning. Theoretical Computer Science 375 (2007)
Raza, M., Gardner, P.: Footprints in local reasoning. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 201–215. Springer, Heidelberg (2008)
Smith, G.: Providing a formal specification for DOM core level 1. PhD Thesis, (to be submitted) (December 2009)
Vafeiadis, V.: Modular fine-grained concurrency verification. Technical Report UCAM-CL-TR-726, Cambridge (2008)
W3C. Dom: Document object model. W3C recommendation (2005), http://www.w3.org/DOM/
Yang, H., O’Hearn, P.W.: A semantic basis for local reasoning. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, p. 402. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gardner, P., Wheelhouse, M. (2010). Small Specifications for Tree Update. In: Laneve, C., Su, J. (eds) Web Services and Formal Methods. WS-FM 2009. Lecture Notes in Computer Science, vol 6194. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14458-5_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-14458-5_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14457-8
Online ISBN: 978-3-642-14458-5
eBook Packages: Computer ScienceComputer Science (R0)