{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T20:47:56Z","timestamp":1743022076775,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642232824"},{"type":"electronic","value":"9783642232831"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-23283-1_12","type":"book-chapter","created":{"date-parts":[[2011,8,24]],"date-time":"2011-08-24T02:30:27Z","timestamp":1314153027000},"page":"154-172","source":"Crossref","is-referenced-by-count":0,"title":["WP Semantics and Behavioral Subtyping"],"prefix":"10.1007","author":[{"given":"Yijing","family":"Liu","sequence":"first","affiliation":[]},{"given":"Zongyan","family":"Qiu","sequence":"additional","affiliation":[]},{"given":"Quan","family":"Long","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","first-page":"2004","volume":"3","author":"M. Barnett","year":"2003","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Leino, K.R.M., Schulte, W., Rustan, K., Leino, M.: Verification of object-oriented programs with invariants. Journal of Object Technology\u00a03, 2004 (2003)","journal-title":"Journal of Object Technology"},{"key":"12_CR2","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":"12_CR3","first-page":"82","volume-title":"Proceedings of the 6th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, PASTE 2005","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: Proceedings of the 6th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, PASTE 2005, pp. 82\u201387. ACM, New York (2005)"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-540-45236-2_24","volume-title":"FME 2003: Formal Methods","author":"L. Burdy","year":"2003","unstructured":"Burdy, L., Requet, A., Lanet, J.-L.: Java applet correctness: A developer-oriented approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 422\u2013439. Springer, Heidelberg (2003)"},{"issue":"8","key":"12_CR5","doi-asserted-by":"publisher","first-page":"713","DOI":"10.1109\/32.879810","volume":"26","author":"A.L.C. Cavalcanti","year":"2000","unstructured":"Cavalcanti, A.L.C., Naumann, D.: A weakest precondition semantics for refinement of object-oriented programs. IEEE Trans. on Software Engineering\u00a026(8), 713\u2013728 (2000)","journal-title":"IEEE Trans. on Software Engineering"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-49019-1_10","volume-title":"Foundations of Software Science and Computation Structures","author":"F.S. Boer de","year":"1999","unstructured":"de Boer, F.S.: A WP-calculus for OO. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol.\u00a01578, pp. 135\u2013149. Springer, Heidelberg (1999), http:\/\/dx.doi.org\/10.1007\/3-540-49019-1_10"},{"key":"12_CR7","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1145\/543552.512558","volume":"37","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. SIGPLAN Not.\u00a037, 234\u2013245 (2002)","journal-title":"SIGPLAN Not."},{"key":"12_CR8","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/BF00276020","volume":"26","author":"W.H. Hesselink","year":"1989","unstructured":"Hesselink, W.H.: Predicate-transformer semantics of general recursion. Acta Informatica\u00a026, 309\u2013332 (1989)","journal-title":"Acta Informatica"},{"key":"12_CR9","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.: Proof of correctness of data representations. Acta Informatica\u00a01, 271\u2013281 (1972)","journal-title":"Acta Informatica"},{"key":"12_CR10","first-page":"2004","volume":"58","author":"B. Jacobs","year":"2002","unstructured":"Jacobs, B.: Weakest precondition reasoning for java programs with jml annotations. Journal of Logic and Algebraic Programming\u00a058, 2004 (2002)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"12_CR11","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/j.tcs.2006.07.034","volume":"365","author":"H. Jifeng","year":"2006","unstructured":"Jifeng, H., Li, X., Liu, Z.: rcos: a refinement calculus of object systems. Theor. Comput. Sci.\u00a0365, 109\u2013142 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"12_CR12","unstructured":"Leavens, G.T., Naumann, D.A.: Behavioral subtyping is equivalent to modular reasoning for object-oriented programs. Technical Report 06-36, Department of Computer Science, Iowa State University, Ames, Iowa, 50011 (December 2006)"},{"key":"12_CR13","unstructured":"Leavens, G.T., Naumann, D.A.: Behavioral subtyping, specification inheritance, and modular reasoning. Technical Report 06-20b, Department of Computer Science, Iowa State University, Ames, Iowa, 50011 (September 2006)"},{"issue":"3","key":"12_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"G.T. Leavens","year":"2006","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. SIGSOFT Software Engineering Notes\u00a031(3), 1\u201338 (2006)","journal-title":"SIGSOFT Software Engineering Notes"},{"key":"12_CR15","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\u2013515. Springer, Heidelberg (2004)"},{"key":"12_CR16","first-page":"17","volume-title":"Addendum to the Proceedings on Object-Oriented Programming Systems, Languages and Applications (Addendum), OOPSLA 1987","author":"B. Liskov","year":"1987","unstructured":"Liskov, B.: Keynote address - data abstraction and hierarchy. In: Addendum to the Proceedings on Object-Oriented Programming Systems, Languages and Applications (Addendum), OOPSLA 1987, pp. 17\u201334. ACM, New York (1987)"},{"issue":"6","key":"12_CR17","doi-asserted-by":"publisher","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"B. Liskov","year":"1994","unstructured":"Liskov, B., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst.\u00a016(6), 1811\u20131841 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/BFb0054091","volume-title":"ECOOP \u201998 - Object-Oriented Programming","author":"J. Noble","year":"1998","unstructured":"Noble, J., Vitek, J., Potter, J.: Flexible alias protection. In: Jul, E. (ed.) ECOOP 1998. LNCS, vol.\u00a01445, pp. 158\u2013185. Springer, Heidelberg (1998)"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/978-3-642-19718-5_23","volume-title":"Programming Languages and Systems","author":"M. Parkinson","year":"2011","unstructured":"Parkinson, M., Summers, A.: The relationship between separation logic and implicit dynamic frames. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol.\u00a06602, pp. 439\u2013458. Springer, Heidelberg (2011)"},{"key":"12_CR21","first-page":"75","volume-title":"Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008","author":"M.J. Parkinson","year":"2008","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic, abstraction and inheritance. In: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, pp. 75\u201386. ACM, New York (2008)"},{"issue":"3","key":"12_CR22","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1016\/j.tcs.2005.06.018","volume":"343","author":"C. Pierik","year":"2005","unstructured":"Pierik, C., de Boer, F.S.: A proof outline logic for object-oriented programming. Theor. Comput. Sci.\u00a0343(3), 413\u2013442 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"12_CR23","first-page":"55","volume-title":"Symposium on Logic in Computer Science","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Symposium on Logic in Computer Science, pp. 55\u201374. IEEE Computer Society, Los Alamitos (2002)"},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-642-03013-0_8","volume-title":"ECOOP 2009 \u2013 Object-Oriented Programming","author":"J. Smans","year":"2009","unstructured":"Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames: Combining dynamic frames and separation logic. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol.\u00a05653, pp. 148\u2013172. Springer, Heidelberg (2009)"},{"key":"12_CR25","unstructured":"Liu, Y., Qiu, Z.: A separation logic for OO programs. Technical Report 2010-42, School of Math., Peking University (2010) (preprints), http:\/\/www.mathinst.pku.edu.cn\/index.php?styleid=2"},{"key":"12_CR26","unstructured":"Liu, Y., Qiu, Z., Long, Q.: A weakest precondition semantics for Java. Technical Report 2010-46, School of Math., Peking University (2010) (preprints), http:\/\/www.mathinst.pku.edu.cn\/index.php?styleid=2"},{"key":"12_CR27","unstructured":"Qiu, Z., Wang, S., Long, Q.: Sequential \u03bcJava: Formal foundations. Technical Report 2007-35, School of Math., Peking University (2007) (preprints), http:\/\/www.mathinst.pku.edu.cn\/index.php?styleid=2"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2011"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-23283-1_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,10]],"date-time":"2024-04-10T13:05:46Z","timestamp":1712754346000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-23283-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642232824","9783642232831"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-23283-1_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}