{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,4]],"date-time":"2025-01-04T16:40:16Z","timestamp":1736008816569,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":52,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540291312"},{"type":"electronic","value":"9783540319399"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11561163_11","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T14:54:31Z","timestamp":1127832871000},"page":"251-273","source":"Crossref","is-referenced-by-count":6,"title":["Assertion-Based Encapsulation, Object Invariants and Simulations"],"prefix":"10.1007","author":[{"given":"David A.","family":"Naumann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-24851-4_1","volume-title":"ECOOP 2004 \u2013 Object-Oriented Programming","author":"J. Aldrich","year":"2004","unstructured":"Aldrich, J., Chambers, C.: Ownership domains: Separating aliasing policy from mechanism. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol.\u00a03086, pp. 1\u201325. Springer, Heidelberg (2004)"},{"key":"11_CR2","unstructured":"Banerjee, A., Naumann, D.A.: Ownership confinement ensures representation independence for object-oriented programs. Journal of the ACM (2002) (Accepted, revision pending. Extended version of [3])"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Banerjee, A., Naumann, D.A.: Representation independence, confinement and access control. In: ACM Symp. on Princ. of Program. Lang (POPL), pp. 166\u2013177 (2002)","DOI":"10.1145\/565816.503289"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/11531142_17","volume-title":"ECOOP 2005 - Object-Oriented Programming","author":"A. Banerjee","year":"2005","unstructured":"Banerjee, A., Naumann, D.A.: State based ownership, reentrance, and encapsulation. In: Black, A.P. (ed.) ECOOP 2005. LNCS, vol.\u00a03586, pp. 387\u2013411. Springer, Heidelberg (2005) (to appear)"},{"issue":"6","key":"11_CR5","doi-asserted-by":"publisher","first-page":"27","DOI":"10.5381\/jot.2004.3.6.a2","volume":"3","author":"M. Barnett","year":"2004","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology\u00a03(6), 27\u201356 (2004) (Special issue: ECOOP 2003 workshop on Formal Techniques for Java-like Programs)","journal-title":"Journal of Object Technology"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Barnett, M., Naumann, D.A.: Friends need a bit more: Maintaining invariants over shared state. In: Kozen, D. (ed.) Mathematics of Program Construction, pp. 54\u201384 (2004)","DOI":"10.1007\/978-3-540-27764-4_5"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Bierman, G., Parkinson, M.: Separation logic and abstraction. In: ACM Symp. on Princ. of Program. Lang (POPL), pp. 247\u2013258 (2005)","DOI":"10.1145\/1047659.1040326"},{"key":"11_CR9","unstructured":"Birkedal, L., Torp-Smith, N.: Higher order separation logic and abstraction (Febraury 2005) (submitted)"},{"issue":"1-3","key":"11_CR10","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.scico.2004.03.003","volume":"52","author":"P. Borba","year":"2004","unstructured":"Borba, P., Sampaio, A., Cavalcanti, A., Corn\u00e9lio, M.: Algebraic reasoning for object-oriented programming. Sci. Comput. Programming\u00a052(1-3), 53\u2013100 (2004)","journal-title":"Sci. Comput. Programming"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/978-3-540-45070-2_20","volume-title":"ECOOP 2003 - Object-Oriented Programming","author":"P.H.M. Borba","year":"2003","unstructured":"Borba, P.H.M., Sampaio, A.C.A., Corn\u00e9lio, M.L.: A refinement algebra for object-oriented programming. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol.\u00a02743, pp. 457\u2013482. Springer, Heidelberg (2003)"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: Preventing data races and deadlocks. In: OOPSLA (2002)","DOI":"10.1145\/582419.582440"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Liskov, B., Shrira, L.: Ownership types for object encapsulation. In: ACM Symp. on Princ. of Program. Lang (POPL), pp. 213\u2013223 (2003)","DOI":"10.1145\/604131.604156"},{"issue":"3","key":"11_CR14","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1016\/S0304-3975(02)00868-X","volume":"298","author":"C. Calcagno","year":"2003","unstructured":"Calcagno, C., O\u2019Hearn, P., Bornat, R.: Program logic and equivalence in the presence of garbage collection. Theoretical Comput. Sci.\u00a0298(3), 557\u2013581 (2003)","journal-title":"Theoretical Comput. Sci."},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1007\/3-540-45614-7_27","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"A.L.C. Cavalcanti","year":"2002","unstructured":"Cavalcanti, A.L.C., Naumann, D.A.: Forward simulation for data refinement of classes. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 471\u2013490. Springer, Heidelberg (2002)"},{"key":"11_CR16","unstructured":"Clarke, D.: Object ownership and containment. Dissertation, Computer Science and Engineering, University of New South Wales, Australia (2001)"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-45337-7_4","volume-title":"ECOOP 2001 - Object-Oriented Programming","author":"D.G. Clarke","year":"2001","unstructured":"Clarke, D.G., Noble, J., Potter, J.M.: Simple ownership types for object containment. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol.\u00a02072, p. 53. Springer, Heidelberg (2001)"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"de Boer, F., Pierik, C.: Computer-aided specification and verification of annotated object-oriented programs. In: Jacobs, B., Rensink, A. (eds.) Formal Methods for Open Object-Based Distributed Systems, pp. 163\u2013177 (2002)","DOI":"10.1007\/978-0-387-35496-5_12"},{"key":"11_CR19","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511663079","volume-title":"Data Refinement: Model-Oriented Proof Methods and their Comparison","author":"W.-P. Roever de","year":"1998","unstructured":"de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, Cambridge (1998)"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"DeLine, R., F\u00e4hndrich, M.: Enforcing high-level protocols in low-level software. In: ACM Conf. on Program. Lang. Design and Implementation (PLDI), pp. 59\u201369 (2001)","DOI":"10.1145\/378795.378811"},{"key":"11_CR21","unstructured":"Detlefs, D.L., Leino, K.R.M., Nelson, G.: Wrestling with rep exposure. Research 156, DEC Systems Research Center (1998)"},{"key":"11_CR22","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software","author":"E. Gamma","year":"1995","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1995)"},{"key":"11_CR23","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C.A.R. Hoare","year":"1972","unstructured":"Hoare, C.A.R.: Proofs of correctness of data representations. Acta Inf\u00a01, 271\u2013281 (1972)","journal-title":"Acta Inf"},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-540-39656-7_8","volume-title":"Formal Methods for Components and Objects","author":"B. Jacobs","year":"2003","unstructured":"Jacobs, B., Kiniry, J., Warnier, M.: Java program verification challenges. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol.\u00a02852, pp. 202\u2013219. Springer, Heidelberg (2003)"},{"key":"11_CR25","unstructured":"Jacobs, B., Leino, K.R.M., Schulte, W.: Multithreaded object-oriented programs with invariants. In: SAVCBS (2004)"},{"key":"11_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-540-39656-7_11","volume-title":"Formal Methods for Components and Objects","author":"G.T. Leavens","year":"2003","unstructured":"Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol.\u00a02852, pp. 262\u2013284. Springer, Heidelberg (2003)"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-24851-4_22","volume-title":"ECOOP 2004 \u2013 Object-Oriented Programming","author":"K.R.M. Leino","year":"2004","unstructured":"Leino, K.R.M., M\u00fcller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol.\u00a03086, pp. 491\u2013516. Springer, Heidelberg (2004)"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., M\u00fcller, P.: Modular verification of static class invariants. In: Formal Methods (2005)","DOI":"10.1007\/11526841_4"},{"key":"11_CR29","volume-title":"Abstraction and Specification in Program Development","author":"B. Liskov","year":"1986","unstructured":"Liskov, B., Guttag, J.: Abstraction and Specification in Program Development. MIT Press, Cambridge (1986)"},{"key":"11_CR30","doi-asserted-by":"crossref","unstructured":"Liskov, B.H., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Prog. Lang. Syst.\u00a016(6) (1994)","DOI":"10.1145\/197320.197383"},{"key":"11_CR31","doi-asserted-by":"crossref","unstructured":"Lynch, N., Vaandrager, F.: Forward and backward simulations part I: Untimed systems. Information and Computation\u00a0121(2) (1995)","DOI":"10.1006\/inco.1995.1134"},{"key":"11_CR32","volume-title":"Object-oriented Software Construction","author":"B. Meyer","year":"1997","unstructured":"Meyer, B.: Object-oriented Software Construction, 2nd edn. Prentice Hall, New York (1997)","edition":"2"},{"key":"11_CR33","unstructured":"Milner, R.: An algebraic definition of simulation between programs. In: Proceedings of Second Intl. Joint Conf. on Artificial Intelligence, pp. 481\u2013489 (1971)"},{"key":"11_CR34","doi-asserted-by":"crossref","unstructured":"Mitchell, J.C.: Representation independence and data abstraction. In: ACM Symp. on Princ. of Program. Lang (POPL), pp. 263\u2013276 (1986)","DOI":"10.1145\/512644.512669"},{"key":"11_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45651-1","volume-title":"Modular Specification and Verification of Object-Oriented Programs","author":"P. M\u00fcller","year":"2002","unstructured":"M\u00fcller, P.: Modular Specification and Verification of Object-Oriented Programs. LNCS, vol.\u00a02262. Springer, Heidelberg (2002)"},{"key":"11_CR36","unstructured":"M\u00fcller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Technical Report 424, Department of Computer Science, ETH Zurich (2004)"},{"key":"11_CR37","doi-asserted-by":"crossref","unstructured":"Naumann, D.A.: Ideal models for pointwise relational and state-free imperative programming. In: Sondergaard, H. (ed.) ACM International Conference on Principles and Practice of Declarative Programming, pp. 4\u201315 (2001)","DOI":"10.1145\/773184.773186"},{"key":"11_CR38","unstructured":"Naumann, D.A.: Patterns and lax lambda laws for relational and imperative programming. Technical Report 2001-2, Computer Science, Stevens Institute of Technology (2001)"},{"issue":"1-2","key":"11_CR39","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/S0304-3975(00)00339-X","volume":"278","author":"D.A. Naumann","year":"2002","unstructured":"Naumann, D.A.: Soundness of data refinement for a higher order imperative language. Theoretical Comput. Sci.\u00a0278(1-2), 271\u2013301 (2002)","journal-title":"Theoretical Comput. Sci."},{"key":"11_CR40","doi-asserted-by":"crossref","unstructured":"Naumann, D.A., Barnett, M.: Towards imperative modules: Reasoning about invariants and sharing of mutable state (extended abstract). In: IEEE Symp. on Logic in Computer Science (LICS), pp. 313\u2013323 (2004)","DOI":"10.1109\/LICS.2004.1319626"},{"key":"11_CR41","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P., Yang, H., Reynolds, J.: Separation and information hiding. In: ACM Symp. on Princ. of Program. Lang (POPL), pp. 268\u2013280 (2004)","DOI":"10.1145\/964001.964024"},{"issue":"3","key":"11_CR42","doi-asserted-by":"publisher","first-page":"658","DOI":"10.1145\/210346.210425","volume":"42","author":"P.W. O\u2019Hearn","year":"1995","unstructured":"O\u2019Hearn, P.W., Tennent, R.D.: Parametricity and local variables. Journal of the ACM\u00a042(3), 658\u2013709 (1995)","journal-title":"Journal of the ACM"},{"key":"11_CR43","doi-asserted-by":"crossref","unstructured":"Pierik, C., Clarke, D., de Boer, F.S.: Controlling object allocation using creation guards. In: Formal Methods 2005 (2005)","DOI":"10.1007\/11526841_6"},{"key":"11_CR44","unstructured":"Pierik, C., de Boer, F.: On behavioral subtyping and completeness. In: ECOOP Workshop on Formal Techniques for Java-like Programs (2005) (to appear)"},{"key":"11_CR45","doi-asserted-by":"crossref","unstructured":"Pierik, C., de Boer, F.S.: A proof outline logic for object-oriented programming. Theoretical Comput. Sci. (2005) (to appear)","DOI":"10.1016\/j.tcs.2005.06.018"},{"key":"11_CR46","first-page":"173","volume-title":"Algol-Like Languages","author":"A.M. Pitts","year":"1997","unstructured":"Pitts, A.M.: Reasoning about local variables with operationally-based logical relations. In: O\u2019Hearn, P.W., Tennent, R.D. (eds.) Algol-Like Languages, vol.\u00a02, ch. 17, pp. 173\u2013193. Birkhauser, Basel (1997); Reprinted from Proceedings Eleventh Annual IEEE Symposium on Logic in Computer Science, Brunswick, NJ (July 1996), pp. 152\u2013163 (1996)"},{"key":"11_CR47","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1017\/S0960129500003066","volume":"10","author":"A.M. Pitts","year":"2000","unstructured":"Pitts, A.M.: Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science\u00a010, 321\u2013359 (2000)","journal-title":"Mathematical Structures in Computer Science"},{"key":"11_CR48","unstructured":"Plotkin, G.: Lambda definability and logical relations. Technical Report SAI-RM-4, University of Edinburgh, School of Artificial Intelligence (1973)"},{"key":"11_CR49","doi-asserted-by":"crossref","unstructured":"Rehof, Mogensen: Tractable constraints in finite semilattices. Sci. Comput. Programming (1996)","DOI":"10.1007\/3-540-61739-6_48"},{"key":"11_CR50","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"11_CR51","doi-asserted-by":"crossref","unstructured":"Skalka, C., Smith, S.: Static use-based object confinement. Springer International Journal of Information Security\u00a04(1-2) (2005)","DOI":"10.1007\/s10207-004-0049-5"},{"key":"11_CR52","volume-title":"Component Software: Beyond Object-Oriented Programming","author":"C. Szyperski","year":"2002","unstructured":"Szyperski, C., Gruntz, D., Murer, S.: Component Software: Beyond Object-Oriented Programming, 2nd edn. ACM Press and Addison-Wesley, New York (2002)","edition":"2"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Components and Objects"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11561163_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,4]],"date-time":"2025-01-04T16:02:26Z","timestamp":1736006546000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11561163_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540291312","9783540319399"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/11561163_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}