{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:06:06Z","timestamp":1770275166354,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":53,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540367499","type":"print"},{"value":"9783540367505","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11804192_16","type":"book-chapter","created":{"date-parts":[[2006,9,29]],"date-time":"2006-09-29T04:20:46Z","timestamp":1159503646000},"page":"342-363","source":"Crossref","is-referenced-by-count":116,"title":["Beyond Assertions: Advanced Specification and Verification with JML and ESC\/Java2"],"prefix":"10.1007","author":[{"given":"Patrice","family":"Chalin","sequence":"first","affiliation":[]},{"given":"Joseph R.","family":"Kiniry","sequence":"additional","affiliation":[]},{"given":"Gary T.","family":"Leavens","sequence":"additional","affiliation":[]},{"given":"Erik","family":"Poll","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"16_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":"16_CR2","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 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":"3","key":"16_CR3","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., 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)"},{"issue":"6","key":"16_CR4","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)","journal-title":"Journal of Object Technology"},{"key":"#cr-split#-16_CR5.1","unstructured":"Bartetzko, D., Fischer, C., M\u00f6ller, M., Wehrheim, H.: Jass \u2014 Java with assertions. In: Workshop on Runtime Verification at CAV 2001 (2001);"},{"key":"#cr-split#-16_CR5.2","unstructured":"Published in ENTCS, Havelund, K., Rosu G. (eds.) vol. 55(2) (2001)"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-45319-9_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Berg van den","year":"2001","unstructured":"van den Berg, J., Jacobs, B.: The LOOP compiler for Java and JML. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 299\u2013312. Springer, Heidelberg (2001)"},{"key":"16_CR7","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)"},{"issue":"10","key":"16_CR8","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"},{"key":"16_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)"},{"key":"16_CR10","unstructured":"Barnett, M., Naumann Wolfram Schulte, D.A., Sun, Q.: 99.44% pure: Useful abstractions in specification. In: Formal Techniques for Java-like Programs (FTfJP 2004), pp. 11\u201319 (May 2004), http:\/\/www.cs.ru.nl\/ftfjp\/2004\/Purity.pdf"},{"key":"16_CR11","unstructured":"Chalin, P.: Towards support for non-null types and non-null-by-default in Java. In: Formal Techniques for Java-like Programs (FTfJP) (to appear, 2006)"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Cok, D.R., Kiniry, J.R.: ESC\/Java2: Uniting ESC\/Java and JML. Technical report, University of Nijmegen, NIII Technical Report NIII-R0413 (2004)","DOI":"10.1007\/978-3-540-30569-9_6"},{"key":"16_CR13","unstructured":"Cheon, Y., Leavens, G.T.: A runtime assertion checker for the Java Modeling Language (JML). In: Arabnia, H.R., Mun, Y. (eds.) The International Conference on Software Engineering Research and Practice (SERP 2002), June 2002, pp. 322\u2013328. CSREA Press (2002)"},{"issue":"6","key":"16_CR14","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:Practice and Experience\u00a035(6), 583\u2013599 (2005)","journal-title":"Software:Practice and Experience"},{"issue":"8","key":"16_CR15","doi-asserted-by":"publisher","first-page":"77","DOI":"10.5381\/jot.2005.4.8.a4","volume":"4","author":"D.R. Cok","year":"2005","unstructured":"David\u00a0R. Cok. Reasoning with specifications containing method calls in JML. Journal of Object Technology, 4(8):77\u2013103, 2005.","journal-title":"Journal of Object Technology"},{"key":"16_CR16","first-page":"258","volume-title":"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: 18th International Conference on Software Engineering, pp. 258\u2013267. IEEE Computer Society Press, Los Alamitos (1996)"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Darvas, \u00c1., M\u00fcller, P.: Reasoning about method calls in JML Specifications. In: Formal Techniques for Java-like Programs (FTfJP) (2005)","DOI":"10.5381\/jot.2006.5.5.a3"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/3-540-46428-X_15","volume-title":"Fundamental Approaches to Software Engineering","author":"K. Huizing","year":"2000","unstructured":"Huizing, K., Kuiper, R.: Verification of object-oriented programs using class invariants. In: Maibaum, T.S.E. (ed.) ETAPS 2000 and FASE 2000. LNCS, vol.\u00a01783, pp. 208\u2013221. Springer, Heidelberg (2000)"},{"issue":"10","key":"16_CR19","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. Communications of the ACM\u00a012(10), 576\u2013583 (1969)","journal-title":"Communications of the ACM"},{"issue":"4","key":"16_CR20","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":"16_CR21","first-page":"137","volume-title":"IEEE International Conference on Software Engineering (SEFM 2005)","author":"B. Jacobs","year":"2005","unstructured":"Jacobs, B., Leino, K.R.M., Piessens, F., Schulte, W.: Safe concurrency for aggregate objects with invariants. In: IEEE International Conference on Software Engineering (SEFM 2005), pp. 137\u2013147. IEEE Computer Society Press, Los Alamitos (2005)"},{"issue":"2","key":"16_CR22","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1109\/MAHC.2003.1203057","volume":"25","author":"C.B. Jones","year":"2003","unstructured":"Jones, C.B.: The early search for tractable ways of reasoning about programs. IEEE Annals of the History of Computing\u00a025(2), 26\u201349 (2003)","journal-title":"IEEE Annals of the History of Computing"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06-rev29, Iowa State University, Department of Computer Science; (January 2006) (to appear) ( ACM SIGSOFT Software Engineering Notes)","DOI":"10.1145\/1127878.1127884"},{"key":"16_CR24","unstructured":"Leavens, G.T., Cheon, Y.: Design by Contract with JML (2005) Draft, available from jmlspecs.org"},{"issue":"1\u20133","key":"16_CR25","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\u20133), 185\u2013208 (2005)","journal-title":"Science of Computer Programming"},{"key":"16_CR26","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)"},{"key":"16_CR27","doi-asserted-by":"crossref","unstructured":"Leavens, G.T.: Modular verification of object-oriented programs with subtypes. Technical Report 90\u201309, Department of Computer Science, Iowa State University, Ames, Iowa, 50011 (July 1990), Available by anonymous ftp from ftp.cs.iastate.edu , and by e-mail from almanac@cs.iastate.edu","DOI":"10.1145\/97945.97970"},{"key":"16_CR28","series-title":"ACM SIGPLAN Notices","first-page":"144","volume-title":"OOPSLA 1998 Conference Proceedings","author":"K. Rustan","year":"1998","unstructured":"Rustan, K., Leino, 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)"},{"key":"16_CR29","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)"},{"key":"#cr-split#-16_CR30.1","doi-asserted-by":"crossref","unstructured":"Liskov, B.: Data abstraction and hierarchy. ACM SIGPLAN Notices\u00a023(5), 17\u201334 (1988);","DOI":"10.1145\/62139.62141"},{"key":"#cr-split#-16_CR30.2","unstructured":"Revised version of the keynote address given at OOPSLA 1987"},{"key":"16_CR31","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)"},{"key":"16_CR32","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D.R., M\u00fcller, P., Kiniry, J.R., Chalin, P.: JML Reference Manual. Department of Computer Science, Iowa State University (January 2006), Available from: http:\/\/www.jmlspecs.org"},{"issue":"6","key":"16_CR33","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 Transactions on Programming Languages and Systems\u00a016(6), 1811\u20131841 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"8","key":"16_CR34","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":"10","key":"16_CR35","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B. Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u201cDesign by Contract\u201d. Computer\u00a025(10), 40\u201351 (1992)","journal-title":"Computer"},{"key":"16_CR36","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":"16_CR37","doi-asserted-by":"crossref","unstructured":"Middelkoop, R., Huizing, C., Kuiper, R., Luit, E.: Cooperation-based invariants for OO languages. In: Proceedings of the International Workshop on Formal Aspects of Component Software (FACS 2005) (2005)","DOI":"10.1016\/j.entcs.2006.05.025"},{"key":"16_CR38","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":"16_CR39","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":"16_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/3-540-46419-0_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Meyer","year":"2000","unstructured":"Meyer, J., Poetzsch-Heffter, A.: An architecture for interactive program provers. In: Schwartzbach, M.I., Graf, S. (eds.) ETAPS 2000 and TACAS 2000. LNCS, vol.\u00a01785, pp. 63\u201377. Springer, Heidelberg (2000)"},{"key":"16_CR41","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1002\/cpe.713","volume":"15","author":"P. M\u00fcller","year":"2003","unstructured":"M\u00fcller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular specification of frame properties in JML. Concurrency, Computation Practice and Experience\u00a015, 117\u2013154 (2003)","journal-title":"Concurrency, Computation Practice and Experience"},{"key":"16_CR42","unstructured":"P. M\u00fcller, A. Poetzsch-Heffter, G.T. Leavens. Modular invariants for layered object structures. Technical Report 424, ETH Zurich (March 2005)"},{"issue":"1\u20132","key":"16_CR43","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\u20132), 89\u2013106 (2004)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"16_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-540-31984-9_15","volume-title":"Fundamental Approaches to Software Engineering","author":"D.A. Naumann","year":"2005","unstructured":"Naumann, D.A.: Observational purity and encapsulation. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol.\u00a03442, pp. 190\u2013204. Springer, Heidelberg (2005)"},{"key":"16_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/BFb0054091","volume-title":"ECOOP 1998 - 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":"16_CR46","unstructured":"Poetzsch-Heffter, A.: Specification and verification of object-oriented programs. Habilitation thesis, Technical University of Munich (January 1997)"},{"key":"16_CR47","doi-asserted-by":"crossref","unstructured":"Ruby, C., Leavens, G.T.: Safely creating correct subclasses without seeing superclass code. In: OOPSLA 2000 Conference on Object-Oriented Programming, Systems, Languages, and Applications, Minneapolis, Minnesota. ACM SIGPLAN Notices, vol.\u00a035(10), pp. 208\u2013228 (October 2000)","DOI":"10.1145\/354222.353186"},{"key":"16_CR48","doi-asserted-by":"crossref","unstructured":"Rosenblum, D.S.: Towards a method of programming with assertions. In: Proceedings of the 14th International Conference on Software Engineering, pp. 92\u2013104 (May 1992)","DOI":"10.1145\/143062.143098"},{"issue":"1","key":"16_CR49","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1109\/32.341844","volume":"21","author":"D.S. Rosenblum","year":"1995","unstructured":"Rosenblum, D.S.: A practical approach to programming with assertions. IEEE Transactions on Software Engineering\u00a021(1), 19\u201331 (1995)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"16_CR50","volume-title":"Component Software","author":"C. Szyperski","year":"1998","unstructured":"Szyperski, C.: Component Software. Addison-Wesley, Reading (1998)"},{"issue":"9","key":"16_CR51","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1109\/2.58215","volume":"23","author":"J.M. Wing","year":"1990","unstructured":"Wing, J.M.: A specifier\u2019s introduction to formal methods. Computer\u00a023(9), 8\u201324 (1990)","journal-title":"Computer"}],"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\/11804192_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,8]],"date-time":"2023-05-08T20:45:49Z","timestamp":1683578749000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11804192_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540367499","9783540367505"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/11804192_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}