{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:52:31Z","timestamp":1740099151576,"version":"3.37.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319980461"},{"type":"electronic","value":"9783319980478"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-98047-8_2","type":"book-chapter","created":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T01:05:49Z","timestamp":1540343149000},"page":"19-39","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Methodology for Invariants, Framing, and Subtyping in JML"],"prefix":"10.1007","author":[{"given":"Yuyan","family":"Bao","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gary T.","family":"Leavens","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,10,24]]},"reference":[{"key":"2_CR1","unstructured":"Pierre America. A Behavioural Approach to Subtyping in Object-Oriented Programming Languages. Tech. rep. 443. Revised from the January 1989 version. Nederlandse Philips Bedrijven B. V.: Philips Research Laboratories, Apr. 1989."},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Anindya Banerjee, David A. Naumann, and Stan Rosenberg. \u201cLocal Reasoning for Global Invariants, Part I: Region Logic\u201d. In: Journal of the ACM 60.3 (June 2013), 18:1\u201318:56. ISSN: 0004-5411. https:\/\/doi.org\/10.1145\/2485982 . URL: http:\/\/doi.acm.org\/10.1145\/2485982 .","DOI":"10.1145\/2485982"},{"key":"2_CR3","unstructured":"Yuyan Bao. \u201cReasoning About Frame Properties in Object-Oriented Programs\u201d. PhD thesis. University of Central Florida, 2017. URL: http:\/\/www.cs.ucf.edu\/~ybao\/tech-reports\/TR_dissertation.pdf ."},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Yuyan Bao, Gary T. Leavens, and Gidon Ernst. \u201cConditional Effects in Fine-grained Region Logic\u201d. In: Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs. FTfJP \u201915. Prague, Czech Republic: ACM, 2015, 5:1\u20135:6. ISBN: 978-1-4503-3656-7. https:\/\/doi.org\/10.1145\/2786536.2786537 . URL: http:\/\/doi.acm.org\/10.1145\/2786536.2786537 .","DOI":"10.1145\/2786536.2786537"},{"issue":"3-4","key":"2_CR5","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/s00165-018-0455-5","volume":"30","author":"Yuyan Bao","year":"2018","unstructured":"Yuyan Bao, Gary T. Leavens, and Gidon Ernst. \u201cUnifying Separation Logic and Region Logic to Allow Interoperability\u201d. In: Formal Aspects of Computing 30.3 (Aug. 2018), pp. 381\u2013441.","journal-title":"Formal Aspects of Computing"},{"key":"2_CR6","first-page":"54","volume-title":"Lecture Notes in Computer Science","author":"Mike Barnett","year":"2004","unstructured":"Mike Barnett and David Naumann. \u201cFriends Need a Bit More: Maintaining Invariants Over Shared State\u201d. In: Mathematics of Program Construction (MPC). Ed. by Dexter Kozen. Vol. 3125. Lecture Notes in Computer Science. Springer-Verlag, July 2004, pp. 54\u201384. URL: http:\/\/www.springerlink.com\/content\/6gt28um7j5jgra12 ."},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Mike Barnett et al. \u201cVerification of Object-Oriented Programs with Invariants\u201d. In: Journal of Object Technology 3.6 (2004), pp. 27\u201356. URL: http:\/\/tinyurl.com\/m2a8j .","DOI":"10.5381\/jot.2004.3.6.a2"},{"issue":"5","key":"2_CR8","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/1095430.1081741","volume":"30","author":"Kevin Bierhoff","year":"2005","unstructured":"Kevin Bierhoff and Jonathan Aldrich. \u201cLightweight Object Specification with Typestates\u201d. In: SIGSOFT Softw. Eng. Notes 30.5 (Sept. 2005), pp. 217\u2013226. ISSN: 0163-5948. https:\/\/doi.org\/10.1145\/1095430.1081741 URL: http:\/\/doi.acm.org\/10.1145\/1095430.1081741 .","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"issue":"10","key":"2_CR9","doi-asserted-by":"publisher","first-page":"785","DOI":"10.1109\/32.469460","volume":"21","author":"A. Borgida","year":"1995","unstructured":"Alex Borgida, John Mylopoulos, and Raymond Reiter. \u201cOn the Frame Problem in Procedure Specifications\u201d. In: IEEE Transactions on Software Engineering 21.10 (Oct. 1995), pp. 785\u2013798. URL: http:\/\/doi.ieeecomputersociety.org\/10.1109\/32.469460 .","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Patrice Chalin et al. \u201cBeyond Assertions: Advanced Specification and Verification with JML and ESC\/Java2\u201d. In: Formal Methods for Components and Objects (FMCO) 2005, Revised Lectures. Vol. 4111. Lecture Notes in Computer Science. Berlin: Springer-Verlag, 2006, pp. 342\u2013363. URL: http:\/\/dx.doi.org\/10.1007\/11804192%5C_16 .","DOI":"10.1007\/11804192"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Robert DeLine and Manuel F\u00e4hndrich. \u201cTypestates for objects\u201d. In: ECOOP 2004 \u2014 Object-Oriented Programming, 18th European Conference. Vol. 3086. Lecture Notes in Computer Science. Springer Verlag, June 2004, pp. 465\u2013490. URL: http:\/\/research.microsoft.com\/apps\/pubs\/default.aspx?id=67463 .","DOI":"10.1007\/978-3-540-24851-4_21"},{"key":"2_CR12","unstructured":"Sophia Drossopoulou, Adrian Francalanza, and Peter M\u00fcller. \u201cA Unified Framework for Verification Techniques for Object Invariants\u201d. In: International Workshop on Foundations of Object-Oriented Languages (FOOL\u201908). 2008. URL: http:\/\/fool08.kuis.kyoto-u.ac.jp\/drossopoulou.pdf ."},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Samin S. Ishtiaq and Peter W. O\u2019Hearn. \u201cBI as an assertion language for mutable data structures\u201d. In: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. POPL \u201901. London, United Kingdom: ACM, 2001, pp. 14\u201326. ISBN: 1-58113-336-7. https:\/\/doi.org\/10.1145\/360204.375719 . URL: http:\/\/doi.acm.org\/10.1145\/360204.375719 .","DOI":"10.1145\/360204.375719"},{"issue":"3","key":"2_CR14","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/s00165-010-0152-5","volume":"23","author":"I. T. Kassios","year":"2010","unstructured":"Ioannis T. Kassios. \u201cThe dynamic frames theory\u201d. In: Formal Aspects of Computing 23.3 (May 2011), pp. 267\u2013288. ISSN: 0934-5043. https:\/\/doi.org\/10.1007\/s00165-010-0152-5 . URL: http:\/\/dx.doi.org\/10.1007\/s00165-010-0152-5 .","journal-title":"Formal Aspects of Computing"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Gary T. Leavens. \u201cJML\u2019s Rich, Inherited Specifications for Behavioral Subtypes\u201d. In: Formal Methods and Software Engineering: 8th International Conference on Formal Engineering Methods (ICFEM). Ed. by Zhiming Liu and He Jifeng. Vol. 4260. Lecture Notes in Computer Science. New York, NY: Springer-Verlag, Nov 2006, pp. 2\u201334. URL: http:\/\/dx.doi.org\/10.1007\/11901433 .","DOI":"10.1007\/11901433"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Gary T. Leavens and Peter M\u00fcller. \u201cInformation Hiding and Visibility in Interface Specifications\u201d. In: International Conference on Software Engineering (ICSE). Los Alamitos, California: IEEE, May 2007, pp. 385\u2013395. URL: http:\/\/dx.doi.org\/10.1109\/ICSE.2007.44 .","DOI":"10.1109\/ICSE.2007.44"},{"issue":"4","key":"2_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2766446","volume":"37","author":"Gary T. Leavens","year":"2015","unstructured":"Gary T. Leavens and David A. Naumann. \u201cBehavioral Subtyping, Specification Inheritance, and Modular Reasoning\u201d. In: TOPLAS 37.4 (Aug. 2015), 13:1\u201313:88. https:\/\/doi.org\/10.1145\/2766446 . URL: http:\/\/doi.acm.org\/10.1145\/2766446 .","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Gary T. Leavens and William E. Weihl. \u201cSpecification and Verification of Object-Oriented Programs Using Supertype Abstraction\u201d. In: Acta Informatica 32.8 (Nov. 1995), pp. 705\u2013778. URL: http:\/\/dx.doi.org\/10.1007\/BF01178658 .","DOI":"10.1007\/BF01178658"},{"key":"2_CR19","unstructured":"Gary T. Leavens et al. \u201cJML Reference Manual\u201d. Available from http:\/\/www.jmlspecs.org . Sept. 2009."},{"key":"2_CR20","unstructured":"K. Rustan M. Leino. \u201cDafny: An Automatic Program Verifier for Functional Correctness\u201d. In: Logic for Programming, Artificial Intelligence, and Reasoning, 16th International Conference, LPAR-16. Vol. 6355. Lecture Notes in Computer Science. Darkar, Senegal: Springer-Verlag, 2010, pp. 348\u2013370."},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"K. Rustan M. Leino. \u201cData groups: Specifying the modification of extended state\u201d. In: OOPSLA \u201998 Conference Proceedings. Vol. 33(10). ACM SIGPLAN Notices. New York, NY: ACM, Oct. 1998, pp. 144\u2013153. URL: http:\/\/doi.acm.org\/10.1145\/286936.286953 .","DOI":"10.1145\/286942.286953"},{"key":"2_CR22","unstructured":"Barbara H. Liskov and Jeannette M. Wing. \u201cA Behavioral Notion of Subtyping\u201d. In: 16.6 (Nov. 1994), pp. 1811\u20131841. URL: http:\/\/doi.acm.org\/10.1145\/197320.197383 ."},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Bertrand Meyer. \u201cApplying \u2018Design by Contract\u201d\u2019. In: Computer 25.10 (Oct. 1992), pp. 40\u201351.","DOI":"10.1109\/2.161279"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Peter M\u00fcller. Modular Specification and Verification of Object-Oriented Programs. Vol. 2262. Lecture Notes in Computer Science. Berlin: Springer-Verlag, 2002. URL: http:\/\/tinyurl.com\/jtwot .","DOI":"10.1007\/3-540-45651-1"},{"issue":"2","key":"2_CR25","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1002\/cpe.713","volume":"15","author":"Peter M\u00fcller","year":"2003","unstructured":"Peter M\u00fcller, Arnd Poetzsch-Heffter, and Gary T. Leavens. \u201cModular Specification of Frame Properties in JML\u201d. In: Concurrency and Computation: Practice and Experience 15.2 (Feb. 2003), pp. 117\u2013154. https:\/\/doi.org\/10.1002\/cpe.713 URL: ftp:\/\/ftp.cs.iastate.edu\/pub\/techreports\/TR02-02\/TR.pdf .","journal-title":"Concurrency and Computation: Practice and Experience"},{"issue":"3","key":"2_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1498926.1498929","volume":"31","author":"Peter W. O'Hearn","year":"2009","unstructured":"Peter W. O\u2019Hearn, Hongseok Yang, and John C. Reynolds. \u201cSeparation and Information Hiding\u201d. In: ACM Trans. Program. Lang. Syst. 31.3 (Apr. 2009), 11:1\u201311:50. ISSN: 0164-0925. https:\/\/doi.org\/10.1145\/1498926.1498929 . URL: http:\/\/doi.acm.org\/10.1145\/1498926.1498929 .","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Matthew Parkinson and Gavin Bierman. \u201cSeparation Logic, Abstraction and Inheritance\u201d. In: ACM Symposium on Principles of Programming Languages. Ed. by Philip Wadler. New York, NY: ACM, Jan. 2008, pp. 75\u201386.","DOI":"10.1145\/1328438.1328451"},{"issue":"12","key":"2_CR28","doi-asserted-by":"publisher","first-page":"1053","DOI":"10.1145\/361598.361623","volume":"15","author":"D. L. Parnas","year":"1972","unstructured":"D. L. Parnas. \u201cOn the Criteria to be Used in Decomposing Systems into Modules\u201d. In: Communications of the ACM 15.12 (Dec. 1972), pp. 1053\u20131058.","journal-title":"Communications of the ACM"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"John C. Reynolds. \u201cSeparation Logic: A Logic for Shared Mutable Data Structures\u201d. In: Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science. Los Alamitos, California: IEEE Computer Society Press, 2002, pp. 55\u201374. URL: http:\/\/dx.doi.org\/10.1109\/LICS.2002.1029817 .","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"3","key":"2_CR30","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s00165-010-0148-1","volume":"22","author":"Jan Smans","year":"2010","unstructured":"Jan Smans et al. \u201cAutomatic verification of Java programs with dynamic frames\u201d. In: Formal Aspects of Computing 22.3 (2010), pp. 423\u2013457. ISSN: 1433-299X. https:\/\/doi.org\/10.1007\/s00165-010-0148-1 . URL: http:\/\/dx.doi.org\/10.1007\/s00165-010-0148-1 .","journal-title":"Formal Aspects of Computing"},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Alexander J. Summers, Sophia Drossopoulou, and Peter M\u00fcller. \u201cThe Need for Flexible Object Invariants\u201d. In: International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming. IWACO \u201909. Genova, Italy: ACM, 2009, 6:1\u20136:9. ISBN: 978-1-60558-546-8. https:\/\/doi.org\/10.1145\/1562154.1562160 . URL: http:\/\/doi.acm.org\/10.1145\/1562154.1562160 .","DOI":"10.1145\/1562154.1562160"},{"key":"2_CR32","unstructured":"Benjamin Wei\u00df. \u201cDeductive Verification of Object-Oriented Software: Dynamic Frames, Dynamic Logic and Predicate Abstraction\u201d. PhD thesis. Karlsruhe Institute of Technology, 2011."}],"container-title":["Principled Software Development"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-98047-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,4]],"date-time":"2022-09-04T14:25:57Z","timestamp":1662301557000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-98047-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319980461","9783319980478"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-98047-8_2","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}