Abstract
A separation context is a client program which does not dereference internals of a module with which it interacts. We use certain “precise” relations to unambiguously describe the storage of a module and prove that separation contexts preserve such relations. We also show that a simulation theorem holds for separation contexts, while this is not the case for arbitrary client programs.
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.
Similar content being viewed by others
References
Hogg, J.: Islands: Aliasing Protection. In: Object-Oriented Languages. In: OOPSLA (1991)
Hogg, J., Lea, D., Wills, A., de Champeaux, D., Holt, R.: The Geneva Convention On The Treatment of Object Aliasing. In: OOPS Messenger (1992)
Banerjee, A., Naumann, D.A.: Representation Independence, Confinement and Access Control [extended abstract]. In: 29th POPL (2002)
Reddy, U.S., Yang, H.: Correctness of Data Representations involving Heap Data Structures. In: Proceedings of ESOP, pp. 223–237. Springer, Heidelberg (2003)
Hoare, C.A.R.: Proof of Correctness of Data Representations. Acta Informatica 1, 271–281 (1972)
He, J., Hoare, C.A.R., Sanders, J.W.: Data Refinement Refined (Resume). In: Proceedings of ESOP. LNCS, vol. 213, pp. 187–196. Springer, Heidelberg (1986)
Clarke, D.G., Noble, J., Potter, J.M.: Simple Ownership Types for Object Containment. In: Proceedings of ECOOP (2001)
Boyapati, C., Liskov, B., Shrira, L.: Ownership Types for Object Encapsulation. In: 30th POPL (2003)
Reynolds, J.C.: Separation Logic: A Logic for Shared Mutable Data Structures. In: Proceedings of 17th LICS, pp. 55–74 (2002)
Pym, D., O’Hearn, P., Yang, H.: Possible Worlds and Resources: The Semantics of BI. Theoretical Computer Science 313(1), 257–305 (2004)
Ishtiaq, S., O’Hearn, P.W.: BI as an Assertion Language for Mutable Data Structures. In: 28th POPL, pp. 14–26 (2001)
O’Hearn, P., Yang, H., Reynolds, J.C.: Separation and information hiding. In: 31st POPL, pp. 268–280 (2004)
Yang, H., O’Hearn, P.: A semantic basis for local reasoning. In: Proceedings of FOSSACS 2002, pp. 402–416 (2002)
Schwarz, J.: Generic Commands - A Tool for Partial Correctness Formalisms. Comput. J. 20(2), 151–155 (1977)
Yang, H.: Relational Separation Logic. Theoretical Computer Science (to appear)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mijajlović, I., Torp-Smith, N., O’Hearn, P. (2004). Refinement and Separation Contexts. In: Lodaya, K., Mahajan, M. (eds) FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2004. Lecture Notes in Computer Science, vol 3328. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30538-5_35
Download citation
DOI: https://doi.org/10.1007/978-3-540-30538-5_35
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-24058-7
Online ISBN: 978-3-540-30538-5
eBook Packages: Computer ScienceComputer Science (R0)