Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions
DOI: 10.1007/11813040_19
关键词:
摘要: 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 shown how a theory with supports features, without use alias control or any other kind restriction. In contrast, approaches introduce number restrictions to programs ensure soundness.
springer.com
sci-hub.st 参考文章(22)
Ioannis T. Kassios, A theory of object oriented refinement University of Toronto. ,(2006)
Mike Barnett, David A. Naumann, Friends Need a Bit More: Maintaining Invariants Over Shared State mathematics of program construction. pp. 54- 84 ,(2004) , 10.1007/978-3-540-27764-4_5
Peter O’Hearn, John Reynolds, Hongseok Yang, Local Reasoning about Programs that Alter Data Structures computer science logic. ,vol. 2142, pp. 1- 19 ,(2001) , 10.1007/3-540-44802-0_1
Ralph-Johan J. Back, D. Gries, F. B. Schneider, Refinement Calculus: A Systematic Introduction ,(1998)
Ioannis T. Kassios, Decoupling in Object Orientation FM 2005: Formal Methods. pp. 43- 58 ,(2005) , 10.1007/11526841_5
K. Rustan M. Leino, Peter Müller, A verification methodology for model fields european symposium on programming. pp. 115- 130 ,(2006) , 10.1007/11693024_9
K. Rustan M. Leino, Peter Müller, Object Invariants in Dynamic Contexts european conference on object-oriented programming. ,vol. 3086, pp. 491- 515 ,(2004) , 10.1007/978-3-540-24851-4_22
Mike Barnett, K. Rustan M. Leino, Wolfram Schulte, The Spec# Programming System: An Overview Construction and Analysis of Safe, Secure, and Interoperable Smart Devices. ,vol. 3362, pp. 49- 69 ,(2005) , 10.1007/978-3-540-30569-9_3
Werner Dietl, Peter Müller, Universes: Lightweight Ownership for JML. The Journal of Object Technology. ,vol. 4, pp. 5- 32 ,(2005) , 10.5381/JOT.2005.4.8.A1
K. Rustan M. Leino, Arnd Poetzsch-Heffter, Yunhong Zhou, Using data groups to specify and check side effects Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation - PLDI '02. ,vol. 37, pp. 246- 257 ,(2002) , 10.1145/512529.512559