Abstract
This paper addresses the frame problem for programming theories that support both sharing and encapsulation through specification variables. The concept of dynamic frames is introduced. It is shown how a programming theory with dynamic frames supports both features, without the use of alias control or any other kind of restriction. In contrast, other approaches introduce a number of restrictions to the programs to ensure soundness.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
References
Back, R., von Wright, J.: Refinement Calculus. A Systematic Introduction. Graduate Texts in Computer Science. Springer, Heidelberg (1998)
Barnett, M., DeLine, R., Fahndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology (2004)
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# specification language: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)
Barnett, M., Naumann, D.: Friends need a bit more: maintaining invariants over shared state. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 54–84. Springer, Heidelberg (2004)
Detlefs, D.L., Leino, K.R.M., Nelson, G.: Wrestling with rep-exposure. Technical Report 156, DEC-SRC (1998)
Dietl, W., Müller, P.: Universes: Lightweight ownership for JML. Journal of Object Technology (to appear, 2005), available on-line at: http://sct.inf.ethz.ch/publications/index.html
O’ Hearn, P., Reynolds, J., Yang, H.: 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)
O’ Hearn, P., Yang, H., Reynolds, J.: Separation and information hiding. In: Proceedings of POPL 2004: Principles of Programming Languages, pp. 268–280 (2004)
Hehner, E.C.R.: A Practical Theory of Programming, Current edn. (2004), available on-line: http://www.cs.toronto.edu/~hehner/aPToP/ (First edition was published by Springer-Verlag in 1993)
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall Series in Computer Science. Prentice-Hall, Englewood Cliffs (1998)
Kassios, I.T.: Object orientation in predicative programming, unification and decoupling in object orientation. Technical Report 500, Computer Systems Research Group, University of Toronto (2004), available online: http://www.cs.toronto.edu/~ykass/work/oopp.ps.gz
Kassios, I.T.: Decoupling in object orientation. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 43–58. Springer, Heidelberg (2005)
Kassios, I.T.: Dynamic frames: Support for framing, dependencies and sharing without restrictions. Technical Report 528, Computer Systems Research Group, University of Toronto (2005), Current version available online: http://www.cs.toronto.edu/~ykass/work/DFcv.ps
Kassios, I.T.: A theory of object oriented refinement. PhD thesis, Dept. of Computer Science, University of Toronto (2006)
Leino, K.R.M.: Data groups: Specifying the modification of extended state. In: OOPSLA 1998 Conference on Object Oriented Programming Systems Languages and Applications, pp. 144–153. ACM, New York (1998)
Leino, K.R.M., Müller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 491–515. Springer, Heidelberg (2004)
Leino, K.R.M., Müller, P.: A verification methodology for model fields. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 115–130. Springer, Heidelberg (2006)
Leino, K.R.M., Nelson, G.: Data abstraction and information hiding. TOPLAS 24(5) (2002)
Leino, K.R.M., Poetzsch-Heffter, A., Zhou, Y.: Using data groups to specify and check side effects. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI 2002). SIGPLAN, vol. 37(5), pp. 246–257. ACM Press, New York (2002)
Müller, P.: Modular Specification and Verification of Object-Oriented Programs. LNCS. Springer, Heidelberg (2002)
Müller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular specification of frame properties in JML. Concurrency Computation Practice and Experience 15, 117–154 (2003)
Parkinson, M., Bierman, G.: Separation logic and abstraction. In: Proceedings of POPL 2005: Principles of Programming Languages, pp. 247–258 (2005)
Reynolds, J.: Separation logic: A logic for shared mutable data structures. In: LICS 2002: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55–74. IEEE Computer Society, Los Alamitos (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kassios, I.T. (2006). Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions. In: Misra, J., Nipkow, T., Sekerinski, E. (eds) FM 2006: Formal Methods. FM 2006. Lecture Notes in Computer Science, vol 4085. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11813040_19
Download citation
DOI: https://doi.org/10.1007/11813040_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37215-8
Online ISBN: 978-3-540-37216-5
eBook Packages: Computer ScienceComputer Science (R0)