{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:00:40Z","timestamp":1740096040492,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":82,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540474609"},{"type":"electronic","value":"9783540474623"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11901433_2","type":"book-chapter","created":{"date-parts":[[2006,11,20]],"date-time":"2006-11-20T12:40:51Z","timestamp":1164026451000},"page":"2-34","source":"Crossref","is-referenced-by-count":36,"title":["JML\u2019s Rich, Inherited Specifications for Behavioral Subtypes"],"prefix":"10.1007","author":[{"given":"Gary T.","family":"Leavens","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/s10270-004-0058-x","volume":"4","author":"W. Ahrendt","year":"2005","unstructured":"Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., H\u00e4hnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool. Software and System Modeling\u00a04, 32\u201354 (2005)","journal-title":"Software and System Modeling"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/3-540-47993-7_25","volume-title":"ECOOP 2002 - Object-Oriented Programming","author":"S. Alagic","year":"2002","unstructured":"Alagic, S., Kouznetsova, S.: Behavioral compatibility of self-typed theories. In: Magnusson, B. (ed.) ECOOP 2002. LNCS, vol.\u00a02374, pp. 585\u2013608. Springer, Heidelberg (2002)"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/3-540-47891-4_22","volume-title":"ECOOP \u201987 European Conference on Object-Oriented Programming","author":"P. America","year":"1987","unstructured":"America, P.: Inheritance and subtyping in a parallel object-oriented language. In: B\u00e9zivin, J., Hullot, J.-M., Lieberman, H., Cointe, P. (eds.) ECOOP 1987. LNCS, vol.\u00a0276, pp. 234\u2013242. Springer, Heidelberg (1987)"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/BFb0019440","volume-title":"Foundations of Object-Oriented Languages","author":"P. America","year":"1991","unstructured":"America, P.: Designing an object-oriented programming language with behavioural subtyping. In: de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1990. LNCS, vol.\u00a0489, pp. 60\u201390. Springer, Heidelberg (1991)"},{"issue":"6","key":"2_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), http:\/\/tinyurl.com\/m2a8j","journal-title":"Journal of Object Technology"},{"issue":"10","key":"2_CR6","doi-asserted-by":"publisher","first-page":"785","DOI":"10.1109\/32.469460","volume":"21","author":"A. Borgida","year":"1995","unstructured":"Borgida, A., Mylopoulos, J., Reiter, R.: On the frame problem in procedure specifications. IEEE Transactions on Software Engineering\u00a021(10), 785\u2013798 (1995)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"3","key":"2_CR7","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1002\/j.1096-9942.1995.tb00019.x","volume":"1","author":"K. Bruce","year":"1995","unstructured":"Bruce, K., Cardelli, L., Castagna, G., Group, T.H.O., Leavens, G.T., Pierce, B.: On binary methods. Theory and Practice of Object Systems\u00a01(3), 221\u2013242 (1995)","journal-title":"Theory and Practice of Object Systems"},{"key":"2_CR8","unstructured":"B\u00fcchi, M., Weck, W.: The greybox approach: When blackbox specifications hide too much. Technical Report 297, Turku Center for Computer Science (August 1999), http:\/\/www.abo.fi\/~mbuechi\/publications\/TR297.html"},{"key":"2_CR9","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":"3","key":"2_CR10","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L. Burdy","year":"2005","unstructured":"Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer (STTT)\u00a07(3), 212\u2013232 (2005)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/3-540-45614-7_16","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"N. Cata\u00f1o","year":"2002","unstructured":"Cata\u00f1o, N., Huisman, M.: Formal specification of Gemplus\u2019s electronic purse case study. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 272\u2013289. Springer, Heidelberg (2002)"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/11804192_16","volume-title":"Formal Methods for Components and Objects","author":"P. Chalin","year":"2006","unstructured":"Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: Advanced specification and verification with JML and ESC\/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 342\u2013363. Springer, Heidelberg (2006), http:\/\/tinyurl.com\/o4nxa"},{"key":"2_CR13","first-page":"91","volume-title":"Foundations of Component-Based Systems","author":"Y. Chen","year":"2000","unstructured":"Chen, Y., Cheng, B.H.C.: A semantic foundation for specification matching. In: Leavens, G.T., Sitaraman, M. (eds.) Foundations of Component-Based Systems, pp. 91\u2013109. Cambridge University Press, New York (2000)"},{"key":"2_CR14","unstructured":"Cheon, Y.: A runtime assertion checker for the Java Modeling Language. Technical Report 03-09, Department of Computer Science, Iowa State University, Ames, IA, The author\u2019s Ph.D. dissertation (April 2003), ftp:\/\/ftp.cs.iastate.edu\/pub\/techreports\/TR03-09\/TR.pdf"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/3-540-47993-7_10","volume-title":"ECOOP 2002 - Object-Oriented Programming","author":"Y. Cheon","year":"2002","unstructured":"Cheon, Y., Leavens, G.T.: A simple and practical approach to unit testing: The JML and JUnit way. In: Magnusson, B. (ed.) ECOOP 2002. LNCS, vol.\u00a02374, pp. 231\u2013255. Springer, Heidelberg (2002)"},{"key":"2_CR16","unstructured":"Cheon, Y., Leavens, G.T.: A runtime assertion checker for the Java Modeling Language (JML). In: Arabnia, H.R., Mun, Y. (eds.) Proceedings of the International Conference on Software Engineering Research and Practice (SERP 2002), Las Vegas, Nevada, USA, June 24-27, pp. 322\u2013328. CSREA Press (2002), ftp:\/\/ftp.cs.iastate.edu\/pub\/techreports\/TR02-05\/TR.pdf"},{"issue":"3","key":"2_CR17","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1145\/196092.195325","volume":"3","author":"Y. Cheon","year":"1994","unstructured":"Cheon, Y., Leavens, G.T.: The Larch\/Smalltalk interface specification language. ACM Transactions on Software Engineering and Methodology\u00a03(3), 221\u2013253 (1994)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"issue":"6","key":"2_CR18","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1002\/spe.649","volume":"35","author":"Y. Cheon","year":"2005","unstructured":"Cheon, Y., Leavens, G.T., Sitaraman, M., Edwards, S.: Model variables: Cleanly supporting abstraction in design by contract. Software\u2014Practice and Experience\u00a035(6), 583\u2013599 (2005)","journal-title":"Software\u2014Practice and Experience"},{"key":"#cr-split#-2_CR19.1","doi-asserted-by":"crossref","unstructured":"Cook, W.R.: Interfaces and specifications for the Smalltalk-80 collection classes. ACM SIGPLAN Notices, 27(10), 1-15 (1992)","DOI":"10.1145\/141937.141938"},{"key":"#cr-split#-2_CR19.2","unstructured":"Paepcke, A. (ed.) OOPSLA 1992 Proceedings (1992)"},{"key":"2_CR20","unstructured":"Dhara, K.K.: Behavioral subtyping in object-oriented languages. Technical Report TR97-09, Department of Computer Science, Iowa State University, 226 Atanasoff Hall, Ames IA 50011-1040. The author\u2019s Ph.D. dissertation (May 1997)"},{"key":"2_CR21","unstructured":"Dhara, K.K., Leavens, G.T.: Preventing cross-type aliasing for more practical reasoning. Technical Report 01-02a, Department of Computer Science, Iowa State University, Ames, Iowa, 50011 (November 2001), available from archives.cs.iastate.edu , ftp:\/\/ftp.cs.iastate.edu\/pub\/techreports\/TR01-02\/TR.pdf"},{"key":"2_CR22","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Mathematical Foundations of Programming Semantics, Eleventh Annual Conference","author":"K.K. Dhara","year":"1995","unstructured":"Dhara, K.K., Leavens, G.T.: Weak behavioral subtyping for types with mutable objects. In: Brookes, S., Main, M., Melton, A., Mislove, M. (eds.) Mathematical Foundations of Programming Semantics, Eleventh Annual Conference. Electronic Notes in Theoretical Computer Science, vol.\u00a01. Elsevier, Amsterdam (1995), available from: http:\/\/www.sciencedirect.com\/science\/journal\/15710661"},{"key":"2_CR23","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1109\/ICSE.1996.493421","volume-title":"Proceedings of the 18th International Conference on Software Engineering","author":"K.K. Dhara","year":"1996","unstructured":"Dhara, K.K., Leavens, G.T.: Forcing behavioral subtyping through specification inheritance. In: Proceedings of the 18th International Conference on Software Engineering, Berlin, Germany, pp. 258\u2013267. IEEE Computer Society Press, Los Alamitos (March 1996), A corrected version is ISU CS TR #95-20c, http:\/\/tinyurl.com\/s2krg"},{"issue":"8","key":"2_CR24","doi-asserted-by":"publisher","first-page":"5","DOI":"10.5381\/jot.2005.4.8.a1","volume":"4","author":"W. Dietl","year":"2005","unstructured":"Dietl, W., M\u00fcller, P.: Universes: Lightweight ownership for JML. Journal of Object Technology (JOT)\u00a04(8), 5\u201332 (2005), http:\/\/www.jot.fm\/issues\/issue_2005_10\/article1.pdf","journal-title":"Journal of Object Technology (JOT)"},{"key":"2_CR25","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Inc., Englewood Cliffs (1976)"},{"issue":"4","key":"2_CR26","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1145\/190679.190682","volume":"19","author":"S.H. Edwards","year":"1994","unstructured":"Edwards, S.H., Heym, W.D., Long, T.J., Sitaraman, M., Weide, B.W.: Part II: Specifying components in RESOLVE. ACM SIGSOFT Software Engineering Notes\u00a019(4), 29\u201339 (1994)","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"issue":"2","key":"2_CR27","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1109\/32.908957","volume":"27","author":"M. Ernst","year":"2001","unstructured":"Ernst, M., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Transactions on Software Engineering\u00a027(2), 99\u2013123 (2001)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"Findler, R.B., Felleisen, M.: Contract soundness for object-oriented languages. In: OOPSLA 2001 Conference Proceedings, Object-Oriented Programming, Systems, Languages, and Applications, Tampa Bay, Florida, USA, October 14-18, pp. 1\u201315 (2001)","DOI":"10.1145\/504311.504283"},{"key":"2_CR29","series-title":"SIGPLAN","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1145\/512529.512558","volume-title":"Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI 2002)","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. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI 2002), June \u00a017\u201319. SIGPLAN, vol.\u00a037(5), pp. 234\u2013245. ACM Press, New York (2002)"},{"key":"2_CR30","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2704-5","volume-title":"Larch: Languages and Tools for Formal Specification","author":"J.V. Guttag","year":"1993","unstructured":"Guttag, J.V., Horning, J.J., Garland, S., Jones, K., Modet, A., Wing, J.: Larch: Languages and Tools for Formal Specification. Springer, New York (1993)"},{"issue":"10","key":"2_CR31","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM\u00a012(10), 576\u2013583 (1969)","journal-title":"Commun. ACM"},{"issue":"4","key":"2_CR32","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(4), 271\u2013281 (1972)","journal-title":"Acta Informatica"},{"key":"2_CR33","unstructured":"Jacobs, B., Poll, E.: Java program verification at Nijmegen: Developments and perspective. Technical Report NIII-R0318, Computing Science Institute, University of Nijmegen (2003), http:\/\/www.cs.kun.nl\/research\/reports\/full\/NIII-R0318.ps.gz"},{"key":"2_CR34","series-title":"ACM SIGPLAN Notices","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1145\/286936.286973","volume-title":"OOPSLA 1998 Conference Proceedings","author":"B. Jacobs","year":"1998","unstructured":"Jacobs, B., van den Berg, J., Huisman, M., van Berkum, M., Hensel, U., Tews, H.: Reasoning about Java classes (preliminary report). In: OOPSLA 1998 Conference Proceedings. ACM SIGPLAN Notices, vol.\u00a033(10), pp. 329\u2013340. ACM, New York (1998)"},{"key":"2_CR35","series-title":"International Series in Computer Science","volume-title":"Systematic Software Development Using VDM","author":"C.B. Jones","year":"1990","unstructured":"Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. International Series in Computer Science. Prentice Hall, Englewood Cliffs (1990)","edition":"2"},{"key":"2_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-30569-9_6","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"J.R. Kiniry","year":"2005","unstructured":"Kiniry, J.R., Cok, D.R.: ESC\/Java2: Uniting ESC\/Java and JML: Progress and issues in building and using ESC\/Java2, including a case study involving the use of the tool to verify portions of an Internet voting tally system. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 108\u2013128. Springer, Heidelberg (2005)"},{"key":"2_CR37","doi-asserted-by":"crossref","unstructured":"LaLonde, W.R., Thomas, D.A., Pugh, J.R.: An exemplar based Smalltalk. ACM SIGPLAN Notices\u00a021(11), 322\u2013330 (1986); In: Meyrowitz, N. (ed.) OOPSLA 1986 Conference Proceedings, Portland, Oregon (September 1986)","DOI":"10.1145\/960112.28729"},{"key":"2_CR38","doi-asserted-by":"crossref","unstructured":"Leavens, G.T.: Verifying object-oriented programs that use subtypes. Technical Report 439, Massachusetts Institute of Technology, Laboratory for Computer Science, The author\u2019s Ph.D. thesis (February 1989)","DOI":"10.21236\/ADA209118"},{"key":"2_CR39","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-0-585-27524-6_8","volume-title":"Specification of Behavioral Semantics in Object-Oriented Information Modeling, ch. 8","author":"G.T. Leavens","year":"1996","unstructured":"Leavens, G.T.: An overview of Larch\/C++: Behavioral specifications for C++ modules. In: Kilov, H., Harvey, W. (eds.) Specification of Behavioral Semantics in Object-Oriented Information Modeling, ch. 8, pp. 121\u2013142. Kluwer Academic Publishers, Boston (1996), An extended version is TR #96-01d, Department of Computer Science, Iowa State University, Ames, Iowa, 50011"},{"key":"2_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1087","DOI":"10.1007\/3-540-48118-4_8","volume-title":"FM\u201999 - Formal Methods","author":"G.T. Leavens","year":"1999","unstructured":"Leavens, G.T., Baker, A.L.: Enhancing the pre- and post condition technique for more expressive specifications. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol.\u00a01709, pp. 1087\u20131106. Springer, Heidelberg (1999), http:\/\/tinyurl.com\/qv84o"},{"key":"2_CR41","first-page":"113","volume-title":"Foundations of Component-Based Systems, ch. 6","author":"G.T. Leavens","year":"2000","unstructured":"Leavens, G.T., Dhara, K.K.: Concepts of behavioral subtyping and a sketch of their extension to component-based systems. In: Leavens, G.T., Sitaraman, M. (eds.) Foundations of Component-Based Systems, ch. 6, pp. 113\u2013135. Cambridge University Press, Cambridge (2000), http:\/\/www.cs.iastate.edu\/~leavens\/FoCBS-book\/06-leavens-dhara.pdf"},{"key":"2_CR42","unstructured":"Leavens, G.T., Naumann, D.A.: Behavioral subtyping, specification inheritance, and modular reasoning. Technical Report 06-20a, Department of Computer Science, Iowa State University, Ames, Iowa, 50011 (August 2006), ftp:\/\/ftp.cs.iastate.edu\/pub\/techreports\/TR06-20\/TR.pdf"},{"issue":"8","key":"2_CR43","doi-asserted-by":"crossref","first-page":"705","DOI":"10.1007\/BF01178658","volume":"32","author":"G.T. Leavens","year":"1995","unstructured":"Leavens, G.T., Weihl, W.E.: Specification and verification of object-oriented programs using supertype abstraction. Acta Informatica\u00a032(8), 705\u2013778 (1995)","journal-title":"Acta Informatica"},{"issue":"1-3","key":"2_CR44","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/j.scico.2004.05.015","volume":"55","author":"G.T. Leavens","year":"2005","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. Science of Computer Programming\u00a055(1-3), 185\u2013208 (2005), http:\/\/dx.doi.org\/10.1016\/j.scico.2004.05.015","journal-title":"Science of Computer Programming"},{"issue":"3","key":"2_CR45","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. ACM SIGSOFT Software Engineering Notes\u00a031(3), 1\u201338 (2006), http:\/\/doi.acm.org\/10.1145\/1127878.1127884","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"2_CR46","unstructured":"Leavens, G.T., Leino, K.R.M., M\u00fcller, P.: Specification and verification challenges for sequential object-oriented programs. Technical Report 06-14, Department of Computer Science, Iowa State University, Ames, Iowa (May 2006), ftp:\/\/ftp.cs.iastate.edu\/pub\/techreports\/TR06-14\/TR.pdf"},{"key":"2_CR47","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D.R., M\u00fcller, P., Kiniry, J., Chalin, P.: JML reference manual. Department of Computer Science, Iowa State University (January 2006), available from: http:\/\/www.jmlspecs.org"},{"key":"2_CR48","unstructured":"Leino, K.R.M.: Toward Reliable Modular Programs. PhD thesis, California Institute of Technology, Available\u00a0as\u00a0Technical\u00a0Report\u00a0Caltech-CS-TR-95-03 (1995)"},{"key":"2_CR49","series-title":"ACM SIGPLAN Notices","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1145\/286936.286953","volume-title":"OOPSLA 1998 Conference Proceedings","author":"K.R.M. Leino","year":"1998","unstructured":"Leino, K.R.M.: Data groups: Specifying the modification of extended state. In: OOPSLA 1998 Conference Proceedings. ACM SIGPLAN Notices, vol.\u00a033(10), pp. 144\u2013153. ACM, New York (1998)"},{"issue":"1-2","key":"2_CR50","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1016\/S0304-3975(98)00165-0","volume":"216","author":"K.R.M. Leino","year":"1999","unstructured":"Leino, K.R.M., Manohar, R.: Joining specification statements. Theoretical Comput. Sci.\u00a0216(1-2), 375\u2013394 (1999)","journal-title":"Theoretical Comput. Sci."},{"key":"2_CR51","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":"2_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11693024_9","volume-title":"Programming Languages and Systems","author":"K.R.M. Leino","year":"2006","unstructured":"Leino, K.R.M., M\u00fcller, P.: A verification methodology for model fields. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol.\u00a03924, pp. 115\u2013130. Springer, Heidelberg (2006), http:\/\/tinyurl.com\/pzll8"},{"issue":"5","key":"2_CR53","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1145\/62139.62141","volume":"23","author":"B. Liskov","year":"1988","unstructured":"Liskov, B.: Data abstraction and hierarchy. ACM SIGPLAN Notices\u00a023(5), 17\u201334 (1988), Revised version of the keynote address given at OOPSLA 1987","journal-title":"ACM SIGPLAN Notices"},{"key":"2_CR54","volume-title":"Program Development in Java","author":"B. Liskov","year":"2001","unstructured":"Liskov, B., Guttag, J.: Program Development in Java. The MIT Press, Cambridge (2001)"},{"issue":"6","key":"2_CR55","doi-asserted-by":"publisher","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"B. Liskov","year":"1994","unstructured":"Liskov, B., Wing, J.: A behavioral notion of subtyping. ACM Trans. Prog. Lang. Syst.\u00a016(6), 1811\u20131841 (1994)","journal-title":"ACM Trans. Prog. Lang. Syst."},{"issue":"10","key":"2_CR56","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1145\/167962.165863","volume":"28","author":"B. Liskov","year":"1993","unstructured":"Liskov, B., Wing, J.M.: Specifications and their use in defining subtypes. ACM SIGPLAN Notices\u00a028(10), 16\u201328 (1993); Paepcke, A. (ed.) OOPSLA 1993 Proceedings (1993)","journal-title":"ACM SIGPLAN Notices"},{"issue":"1-2","key":"2_CR57","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.jlap.2003.07.006","volume":"58","author":"C. March\u00e9","year":"2004","unstructured":"March\u00e9, C., Paulin-Mohring, C., Urbain, X.: The KRAKATOA tool for certification of JAVA\/JAVACARD programs annotated in JML. Journal of Logic and Algebraic Programming\u00a058(1-2), 89\u2013106 (2004)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"2_CR58","series-title":"Object-Oriented Series","volume-title":"Eiffel: The Language","author":"B. Meyer","year":"1992","unstructured":"Meyer, B.: Eiffel: The Language. Object-Oriented Series. Prentice Hall, New York (1992)"},{"key":"2_CR59","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":"2_CR60","volume-title":"Design by Contract by Example","author":"R. Mitchell","year":"2002","unstructured":"Mitchell, R., McKim, J.: Design by Contract by Example. Addison-Wesley, Indianapolis (2002)"},{"key":"2_CR61","volume-title":"Programming from Specifications","author":"C. Morgan","year":"1994","unstructured":"Morgan, C.: Programming from Specifications, 2nd edn. Prentice Hall International, Hempstead (1994)","edition":"2"},{"key":"2_CR62","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. In: M\u00fcller, P. (ed.) Modular Specification and Verification of Object-Oriented Programs. LNCS, vol.\u00a02262. Springer, Heidelberg (2002), http:\/\/tinyurl.com\/jtwot"},{"issue":"3","key":"2_CR63","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/j.scico.2006.03.001","volume":"62","author":"P. M\u00fcller","year":"2006","unstructured":"M\u00fcller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Sci. Comput. Programming\u00a062(3), 253\u2013286 (2006), http:\/\/dx.doi.org\/10.1016\/j.scico.2006.03.001","journal-title":"Sci. Comput. Programming"},{"key":"2_CR64","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/S0020-0190(00)00215-5","volume":"77","author":"D.A. Naumann","year":"2001","unstructured":"Naumann, D.A.: Calculating sharp adaptation rules. Inf. Process. Lett.\u00a077, 201\u2013208 (2001)","journal-title":"Inf. Process. Lett."},{"key":"2_CR65","doi-asserted-by":"crossref","unstructured":"Naumann, D.A., Barnett, M.: Towards imperative modules: Reasoning about invariants and sharing of mutable state. Theoretical Comput. Sci (to appear, 2006)","DOI":"10.1016\/j.tcs.2006.07.035"},{"key":"2_CR66","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)"},{"issue":"4","key":"2_CR67","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/190679.190681","volume":"19","author":"W.F. Ogden","year":"1994","unstructured":"Ogden, W.F., Sitaraman, M., Weide, B.W., Zweben, S.H.: Part I: The RESOLVE framework and discipline \u2014 a research synopsis. ACM SIGSOFT Software Engineering Notes\u00a019(4), 23\u201328 (1994)","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"2_CR68","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/0304-3975(83)90009-9","volume":"24","author":"E. Olderog","year":"1983","unstructured":"Olderog, E.: On the notion of expressiveness and the rule of adaptation. Theoretical Comput. Sci.\u00a024, 337\u2013347 (1983)","journal-title":"Theoretical Comput. Sci."},{"key":"2_CR69","unstructured":"Parkinson, M.J.: Local reasoning for Java. Technical Report 654, University of Cambridge Computer Laboratory, (November 2005), The author\u2019s Ph.D. dissertation, http:\/\/www.cl.cam.ac.uk\/TechReports\/UCAM-CL-TR-654.pdf"},{"key":"2_CR70","unstructured":"Pierik, C.: Validation Techniques for Object-Oriented Proof Outlines. PhD thesis, Universiteit Utrecht (2006), http:\/\/igitur-archive.library.uu.nl\/dissertations\/2006-0502-200341\/index.htm"},{"key":"2_CR71","unstructured":"Poetzsch-Heffter, A.: Specification and verification of object-oriented programs. Habilitation thesis, Technical University of Munich (January 1997), http:\/\/tinyurl.com\/g7xgm"},{"key":"2_CR72","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-49099-X_11","volume-title":"Programming Languages and Systems","author":"A. Poetzsch-Heffter","year":"1999","unstructured":"Poetzsch-Heffter, A., M\u00fcller, P.: A programming logic for sequential Java. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol.\u00a01576, pp. 162\u2013176. Springer, Heidelberg (1999), http:\/\/tinyurl.com\/krjle"},{"key":"2_CR73","unstructured":"Poetzsch-Heffter, A., M\u00fcller, P., Sch\u00e4fer, J.: The Jive tool (April 2006) (Checked August 2), http:\/\/softech.informatik.uni-kl.de\/twiki\/bin\/view\/Homepage\/Jive"},{"key":"2_CR74","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Coalgebraic Methods in Computer Science (CMCS)","author":"E. Poll","year":"2000","unstructured":"Poll, E.: A coalgebraic semantics of subtyping. In: Reichel, H. (ed.) Coalgebraic Methods in Computer Science (CMCS). Electronic Notes in Theoretical Computer Science. vol.\u00a033. Elsevier, Amsterdam (2000)"},{"key":"2_CR75","unstructured":"Raghavan, A.D., Leavens, G.T.: Desugaring JML method specifications. Technical Report 00-03e, Iowa State University, Department of Computer Science (May 2005), ftp:\/\/ftp.cs.iastate.edu\/pub\/techreports\/TR00-03\/TR.pdf"},{"key":"2_CR76","series-title":"SIGSOFT Softw. Eng. Notes","first-page":"267","volume-title":"Proceedings of the 9th European Software Engineering Conference held jointly with the 11th ACM SIGSOFT Symposium on the Foundations of Software Engineering","author":"E.R. Robby","year":"2003","unstructured":"Robby, E.R., Dwyer, M.B., Hatcliff, J.: Bogor: An extensible and highly-modular model checking framework. In: Proceedings of the 9th European Software Engineering Conference held jointly with the 11th ACM SIGSOFT Symposium on the Foundations of Software Engineering. SIGSOFT Softw. Eng. Notes, vol.\u00a028(5), pp. 267\u2013276. ACM, New York (2003)"},{"key":"2_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-540-24730-2_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E.R. Robby","year":"2004","unstructured":"Robby, E.R., Dwyer, M., Hatcliff, J.: Checking strong specifications using an extensible software model checking framework. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 404\u2013420. Springer, Heidelberg (2004)"},{"key":"2_CR78","doi-asserted-by":"crossref","unstructured":"Stepney, S., Barden, R., Cooper, D. (eds.): Object Orientation in Z. Workshops in Computing. Springer, Cambridge (1992)","DOI":"10.1007\/978-1-4471-3552-4"},{"key":"2_CR79","unstructured":"Specification in Fresco. In: Stepney, et al., [78], ch. 11, pp. 127\u2013135"},{"key":"2_CR80","unstructured":"Wing, J.M.: A two-tiered approach to specifying programs. Technical Report TR-299, Massachusetts Institute of Technology, Laboratory for Computer Science (1983)"},{"issue":"1","key":"2_CR81","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/9758.10500","volume":"9","author":"J.M. Wing","year":"1987","unstructured":"Wing, J.M.: Writing Larch interface language specifications. ACM Trans. Prog. Lang. Syst.\u00a09(1), 1\u201324 (1987)","journal-title":"ACM Trans. Prog. Lang. Syst."}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11901433_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,19]],"date-time":"2020-04-19T01:30:49Z","timestamp":1587259849000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11901433_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540474609","9783540474623"],"references-count":82,"URL":"https:\/\/doi.org\/10.1007\/11901433_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}