{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:12:38Z","timestamp":1770282758801,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":87,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540203032","type":"print"},{"value":"9783540396567","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39656-7_11","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T18:35:52Z","timestamp":1277836552000},"page":"262-284","source":"Crossref","is-referenced-by-count":43,"title":["How the Design of JML Accommodates Both Runtime Assertion Checking and Formal Verification"],"prefix":"10.1007","author":[{"given":"Gary T.","family":"Leavens","sequence":"first","affiliation":[]},{"given":"Yoonsik","family":"Cheon","sequence":"additional","affiliation":[]},{"given":"Curtis","family":"Clifton","sequence":"additional","affiliation":[]},{"given":"Clyde","family":"Ruby","sequence":"additional","affiliation":[]},{"given":"David R.","family":"Cok","sequence":"additional","affiliation":[]}],"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-39656-7_1","volume-title":"Formal Methods for Components and Objects","author":"E. Abraham-Mumm","year":"2003","unstructured":"Abraham-Mumm, E., de Boer, F.S., de Roever, W.P., Steffen, M.: A toolsupported proof system for mutlithreaded java. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol.\u00a02852, pp. 1\u201332. Springer, Heidelberg (2003)"},{"key":"11_CR2","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":"11_CR3","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":"3","key":"11_CR4","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/BF00264250","volume":"21","author":"H. Barringer","year":"1984","unstructured":"Barringer, H., Cheng, J.H., Jones, C.B.: A logic covering undefinedness in program proofs. Acta Informatica\u00a021(3), 251\u2013269 (1984)","journal-title":"Acta Informatica"},{"key":"11_CR5","unstructured":"Bartetzko, D., Fischer, C., Moller, M., Wehrheim, H.: Jass - Java with assertions. In: Havelund, K., Rosu, G. (eds.) Workshop on Runtime Verification held in conjunction with the 13th Conference on Computer Aided Verification, CAV 2001. Published in Electronic Notes in Theoretical Computer Science, vol.\u00a055(2) (2001), Available from www.elsevier.nl"},{"key":"11_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-2033-9","volume-title":"Proof in VDM: A Practitioner\u2019s Guide","author":"J. Bicarregui","year":"1994","unstructured":"Bicarregui, J., Fitgerald, J.S., Lindsay, P.A., Moore, R., Ritchie, B.: Proof in VDM: A Practitioner\u2019s Guide. Springer, New York (1994)"},{"key":"11_CR7","series-title":"Object Technology Series","volume-title":"The Unified Modeling Language User Guide","author":"G. Booch","year":"1999","unstructured":"Booch, G., Rumbaugh, J., Jacobson, I.: The Unified Modeling Language User Guide. Object Technology Series. Addison Wesley, Reading (1999)"},{"key":"11_CR8","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/566172.566191","volume-title":"Proceedings International Symposium on Software Testing and Analysis (ISSTA)","author":"C. Boyapati","year":"2002","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: Automated testing based on Java predicates. In: Proceedings International Symposium on Software Testing and Analysis (ISSTA), July 2002, pp. 123\u2013133. ACM, New York (2002)"},{"key":"11_CR9","unstructured":"Chalin, P.: Back to basics: Language support and semantics of basic infinite integer types in JML and Larch. Technical Report CU-CS 2002-003.1, Computer Science Department, Concordia University (October 2002)"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Chalin, P.: Improving JML: For a safer and more effective language. Technical Report 2003-001.1, Computer Science Department, Concordia University (March 2003)","DOI":"10.1007\/978-3-540-45236-2_25"},{"issue":"3","key":"11_CR11","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":"11_CR12","first-page":"39","volume":"7","author":"Y. Cheon","year":"1994","unstructured":"Cheon, Y., Leavens, G.T.: A quick overview of Larch\/C++. Journal of Object-Oriented Programming\u00a07(6), 39\u201349 (1994)","journal-title":"Journal of Object-Oriented Programming"},{"key":"11_CR13","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)"},{"key":"11_CR14","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":"11_CR15","doi-asserted-by":"crossref","unstructured":"Clifton, C.: MultiJava: Design, implementation, and evaluation of a Javacompatible language supporting modular open classes and symmetric multiple dispatch. Technical Report 01-10, Department of Computer Science, Iowa State University, Ames, Iowa, 50011 (November 2001), Available from http:\/\/www.multijava.org","DOI":"10.1145\/354222.353181"},{"key":"11_CR16","series-title":"ACM SIGPLAN Notices","first-page":"130","volume-title":"OOPSLA 2000 Conference on Object-Oriented Programming, Systems, Languages, and Applications","author":"C. Clifton","year":"2000","unstructured":"Clifton, C., Leavens, G.T., Chambers, C., Millstein, T.: MultiJava: Modular open classes and symmetric multiple dispatch for Java. In: OOPSLA 2000 Conference on Object-Oriented Programming, Systems, Languages, and Applications, October 2000. ACM SIGPLAN Notices, vol.\u00a035(10), pp. 130\u2013145. ACM, New York (2000)"},{"key":"11_CR17","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4613-9706-9","volume-title":"Programming in the 1990s: An Introduction to the Calculation of Programs","author":"E. Cohen","year":"1990","unstructured":"Cohen, E.: Programming in the 1990s: An Introduction to the Calculation of Programs. Springer, New York (1990)"},{"key":"11_CR18","unstructured":"Detlefs, D.L., Rustan, K., Leino, M., Nelson, G., Saxe, J.B.: Extended static checking. SRC Research Report 159, Compaq Systems Research Center, 130 Lytton Ave., Palo Alto (December 1998)"},{"key":"11_CR19","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, March 1996, pp. 258\u2013267. IEEE Computer Society Press, Los Alamitos (1996); A corrected version is Iowa State University, Dept. of Computer Science TR #95-20c"},{"key":"11_CR20","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate Calculus and program semantics","author":"E.W. Dijkstra","year":"1990","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and program semantics. Springer, NY (1990)"},{"key":"11_CR21","unstructured":"Duncan, A., Holzle, U.: Adding contracts to Java with Handshake. Technical Report TRCS98-32, Department of Computer Science, University of California, Santa Barbara, CA (December 1998)"},{"issue":"4","key":"11_CR22","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":"11_CR23","doi-asserted-by":"publisher","first-page":"1","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), 1\u201325 (2001)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Findler, R.B., Felleisen, M.: Contract soundness for objectoriented 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":"11_CR25","doi-asserted-by":"crossref","unstructured":"Findler, R.B., Latendresse, M., Felleisen, M.: Behavioral contracts and behavioral subtyping. In: Proceedings of Joint 8th European Software Engineering Conference (ESEC) and 9th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE), Vienna, Austria, September 10-14 (2001)","DOI":"10.1145\/503209.503240"},{"issue":"2","key":"11_CR26","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1109\/32.485225","volume":"22","author":"K. Finney","year":"1996","unstructured":"Finney, K.: Mathematical notation in formal specification: Too difficult for the masses? IEEE Transactions on Software Engineering\u00a022(2), 158\u2013159 (1996)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"11_CR27","unstructured":"Fitzgerald, J., Larsen, P.G.: Modelling Systems: Practical Tools in Software Development, Cambridge, UK (1998)"},{"key":"11_CR28","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., Rustan, K., Leino, M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Norris, C., Fenwick Jr., J.B. (eds.) Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI 2002), June 17-19. SIGPLAN, vol.\u00a037(5), pp. 234\u2013245. ACM Press, New York (2002)"},{"key":"11_CR29","first-page":"151","volume-title":"Proceedings of the International Workshop on Hypermedia Design (IWHD 1995)","author":"L. Friendly","year":"1995","unstructured":"Friendly, L.: The design of distributed hyperlinked programming documentation. In: Fra\u00efss\u00e8, S., Garzotto, F., Isakowitz, T., Nanard, J., Nanard, M. (eds.) Proceedings of the International Workshop on Hypermedia Design (IWHD 1995), Montpellier, France, June 1-2, pp. 151\u2013173. Springer, Heidelberg (1995)"},{"key":"11_CR30","first-page":"28","volume-title":"ACM Conference on LISP and Functional Programming","author":"D.K. Gifford","year":"1986","unstructured":"Gifford, D.K., Lucassen, J.M.: Integrating functional and imperative programming. In: ACM Conference on LISP and Functional Programming, August 1986, pp. 28\u201338. ACM, New York (1986)"},{"key":"11_CR31","series-title":"Texts and Monographs in Computer Science","volume-title":"A Logical Approach to Discrete Math","author":"D. Gries","year":"1994","unstructured":"Gries, D., Schneider, F.B.: A Logical Approach to Discrete Math. Texts and Monographs in Computer Science. Springer, New York (1994)"},{"key":"11_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/BFb0015254","volume-title":"Computer Science Today","author":"D. Gries","year":"1995","unstructured":"Gries, D., Schneider, F.B.: Avoiding the undefined by underspecification. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol.\u00a01000, pp. 366\u2013373. Springer, Heidelberg (1995)"},{"key":"11_CR33","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.J., Jones, K.D., Modet, A., Wing, J.M.: Larch: Languages and Tools for Formal Specification. Springer, New York (1993)"},{"issue":"10","key":"11_CR34","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"},{"key":"11_CR35","first-page":"83","volume-title":"Structured Programming","author":"C.A.R. Hoare","year":"1972","unstructured":"Hoare, C.A.R.: Notes on data structuring. In: Dijkstra, E., Dahl, O.-J., Hoare, C.A.R. (eds.) Structured Programming, pp. 83\u2013174. Academic Press, Inc., New York (1972)"},{"issue":"4","key":"11_CR36","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":"11_CR37","unstructured":"Huisman, M.: Reasoning about Java Programs in higher order logic with PVS and Isabelle, February 2001. Ipa dissertation series 2001-03. University of Nijmegen, Holland (2001)"},{"key":"11_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-46428-X_20","volume-title":"Fundamental Approaches to Software Engineering","author":"M. Huisman","year":"2000","unstructured":"Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol.\u00a01783, pp. 284\u2013303. Springer, Heidelberg (2000); An earlier version is technical report CSI-R9912"},{"issue":"2","key":"11_CR39","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D. Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: A lightweight object modeling notation. ACM Transactions on Software Engineering and Methodology\u00a011(2), 256\u2013290 (2002)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"11_CR40","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_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-45314-8_21","volume-title":"Fundamental Approaches to Software Engineering","author":"B. Jacobs","year":"2001","unstructured":"Jacobs, B., Poll, E.: A logic for the Java modeling language JML. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol.\u00a02029, pp. 284\u2013299. Springer, Heidelberg (2001)"},{"key":"11_CR42","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, October 1998. ACM SIGPLAN Notices, vol.\u00a033(10), pp. 329\u2013340. ACM, New York (1998)"},{"key":"11_CR43","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":"11_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-54834-3_26","volume-title":"VDM \u201991","author":"H.B.M. Jonkers","year":"1991","unstructured":"Jonkers, H.B.M.: Upgrading the pre- and postcondition technique. In: Prehn, S., Toetenel, H. (eds.) VDM 1991. LNCS, vol.\u00a0551, pp. 428\u2013456. Springer, Heidelberg (1991)"},{"key":"11_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/3-540-48443-4_18","volume-title":"Meta-Level Architectures and Reflection","author":"M. Karaorman","year":"1999","unstructured":"Karaorman, M., Holzle, U., Bruno, J.: jContractor: A reflective Java library to support design by contract. In: Cointe, P. (ed.) Reflection 1999. LNCS, vol.\u00a01616, pp. 175\u2013196. Springer, Heidelberg (1999)"},{"key":"11_CR46","series-title":"SIGPLAN Notices","first-page":"231","volume-title":"Proceedings of OOPSLA 2002 Conference on Object-Oriented Programming, Languages, Systems, and Applications","author":"S. Khurshid","year":"2002","unstructured":"Khurshid, S., Marinov, D., Jackson, D.: An analyzable annotation language. In: Proceedings of OOPSLA 2002 Conference on Object-Oriented Programming, Languages, Systems, and Applications, November 2002. SIGPLAN Notices, vol.\u00a037(11), pp. 231\u2013245. ACM, New York (2002)"},{"key":"11_CR47","doi-asserted-by":"crossref","unstructured":"Kramer, R.: iContract \u2013 the Java design by contract tool. In: TOOLS 26: Technology of Object-Oriented Languages and Systems, Los Alamitos, California, pp. 295\u2013307 (1998)","DOI":"10.1109\/TOOLS.1998.711021"},{"issue":"1","key":"11_CR48","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1145\/63238.63240","volume":"32","author":"L. Lamport","year":"1989","unstructured":"Lamport, L.: A simple approach to specifying concurrent systems. Communications of the ACM\u00a032(1), 32\u201345 (1989)","journal-title":"Communications of the ACM"},{"key":"11_CR49","volume-title":"Applying UML and Patterns: An Introduction to Object-Oriented Analysis and Design and the Unified Process","author":"C. Larman","year":"2002","unstructured":"Larman, C.: Applying UML and Patterns: An Introduction to Object-Oriented Analysis and Design and the Unified Process, 2nd edn. Prentice Hall PTR, Upper Saddle River (2002)","edition":"2"},{"key":"11_CR50","series-title":"ch. 8","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","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":"11_CR51","unstructured":"Leavens, G.T.: Larch\/C++ Reference Manual. Version 5.41, Available in ftp: http:\/\/www.ftp.cs.iastate.edu\/pub\/larchc++\/lcpp.ps.gz or on the World Wide Web at the URL http:\/\/www.cs.iastate.edu\/~leavens\/larchc++.html (April 1999)"},{"key":"11_CR52","unstructured":"Leavens, G.T.: Larch frequently asked questions. Version 1.110 (May 2000), Available in http:\/\/www.cs.iastate.edu\/~leavens\/larch-faq.html"},{"key":"11_CR53","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 postcondition 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)"},{"key":"11_CR54","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-1-4615-5229-1_12","volume-title":"Behavioral Specifications of Businesses and Systems","author":"G.T. Leavens","year":"1999","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems, pp. 175\u2013188. Kluwer Academic Publishers, Boston (1999)"},{"key":"11_CR55","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06v, Iowa State University, Department of Computer Science (May 2003), See http:\/\/www.jmlspecs.org"},{"key":"11_CR56","first-page":"159","volume-title":"Proceedings of the First International Workshop on Larch, July, 1992, Workshops in Computing","author":"G.T. Leavens","year":"1993","unstructured":"Leavens, G.T., Cheon, Y.: Preliminary design of Larch\/C++. In: Martin, U., Wing, J. (eds.) Proceedings of the First International Workshop on Larch, July, 1992, Workshops in Computing, pp. 159\u2013184. Springer, New York (1993)"},{"key":"11_CR57","series-title":"ch. 6","first-page":"113","volume-title":"Foundations of Component-Based Systems","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":"11_CR58","first-page":"105","volume-title":"OOPSLA 2000 Companion, Minneapolis, Minnesota","author":"G.T. Leavens","year":"2000","unstructured":"Leavens, G.T., Leino, K.R.M., Poll, E., Ruby, C., Jacobs, B.: JML: notations and tools supporting detailed design in Java. In: OOPSLA 2000 Companion, Minneapolis, Minnesota, October 2000, pp. 105\u2013106. ACM, New York (2000)"},{"key":"11_CR59","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1007\/s002360050168","volume":"36","author":"G.T. Leavens","year":"2000","unstructured":"Leavens, G.T., Pigozzi, D.: A complete algebraic characterization of behavioral subtyping. Acta Informatica\u00a036, 617\u2013663 (2000)","journal-title":"Acta Informatica"},{"key":"11_CR60","series-title":"ACM SIGPLAN Notices","first-page":"212","volume-title":"OOPSLA ECOOP 1990 Proceedings","author":"G.T. Leavens","year":"1990","unstructured":"Leavens, G.T., Weihl, W.E.: Reasoning about object-oriented programs that use subtypes (extended abstract). In: Meyrowitz, N. (ed.) OOPSLA ECOOP 1990 Proceedings, October 1990. ACM SIGPLAN Notices, vol.\u00a025(10), pp. 212\u2013223. ACM, New York (1990)"},{"issue":"8","key":"11_CR61","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 objectoriented programs using supertype abstraction. Acta Informatica\u00a032(8), 705\u2013778 (1995)","journal-title":"Acta Informatica"},{"key":"11_CR62","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/PL00003926","volume":"10","author":"G.T. Leavens","year":"1998","unstructured":"Leavens, G.T., Wing, J.M.: Protective interface specifications. Formal Aspects of Computing\u00a010, 59\u201375 (1998)","journal-title":"Formal Aspects of Computing"},{"key":"11_CR63","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":"11_CR64","unstructured":"Rustan, K., Leino, M.: A myth in the modular specification of programs. Technical Report KRML 63, Digital Equipment Corporation, Systems Research Center, 130 Lytton Avenue Palo Alto, CA 94301, Obtain from the author at leino@microsoft.com (November 1995)"},{"key":"11_CR65","unstructured":"Rustan, K., Leino, M., Nelson, G., Saxe, J.B.: ESC\/Java user\u2019s manual. Technical note, Compaq Systems Research Center (October 2000)"},{"key":"11_CR66","unstructured":"Rustan, K., Leino, M., Saxe, J.B., Stata, R.: Checking Java programs via guarded commands. Technical Note 1999-002, Compaq Systems Research Center, Palo Alto, CA (May 1999)"},{"issue":"10","key":"11_CR67","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/383845.383855","volume":"44","author":"K. Lieberherr","year":"2001","unstructured":"Lieberherr, K., Orleans, D., Ovlinger, J.: Aspect-oriented programming with adaptive methods. Communications of the ACM\u00a044(10), 39\u201341 (2001)","journal-title":"Communications of the ACM"},{"key":"11_CR68","volume-title":"Abstraction and Specification in Program Development","author":"B. Liskov","year":"1986","unstructured":"Liskov, B., Guttag, J.: Abstraction and Specification in Program Development. The MIT Press, Cambridge (1986)"},{"issue":"6","key":"11_CR69","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"},{"key":"11_CR70","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":"11_CR71","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_CR72","volume-title":"Proceedings of RV 2001, First Workshop on Runtime Verification","author":"J.W. Nimmer","year":"2001","unstructured":"Nimmer, J.W., Ernst, M.D.: Static verification of dynamically detected program invariants: Integrating Daikon and ESC\/Java. In: Proceedings of RV 2001, First Workshop on Runtime Verification. Elsevier, Amsterdam (July 2001); To appear in Electronic Notes in Theoretical Computer Science"},{"issue":"4","key":"11_CR73","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":"11_CR74","unstructured":"International Standards Organization. Information technology \u2013 programming languages, their environments and system software interfaces \u2013 Vienna Development Method \u2013 specification language \u2013 part 1: Base language. ISO\/IEC 13817-1 (December 1996)"},{"key":"11_CR75","unstructured":"Parasoft Corporation. Using design by contract TM to automate Java TM software and component testing, Available from http:\/\/www.parasoft.com\/jsp\/products\/tech_papers.jsp?product=Jcontract (as of February 2003)"},{"key":"11_CR76","unstructured":"Raghavan, A.D., Leavens, G.T.: Desugaring JML method specifications. Technical Report 00-03c, Iowa State University, Department of Computer Science (August 2001)"},{"key":"11_CR77","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, May 1992, pp. 92\u2013104 (1992)","DOI":"10.1145\/143062.143098"},{"key":"11_CR78","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, October 2000. ACM SIGPLAN Notices, vol.\u00a035(10), pp. 208\u2013228 (2000)","DOI":"10.1145\/354222.353186"},{"key":"11_CR79","doi-asserted-by":"crossref","unstructured":"Spivey, J.: An introduction to Z and formal specifications. Software Engineering Journal (January 1989)","DOI":"10.1049\/sej.1989.0006"},{"key":"11_CR80","series-title":"International Series in Computer Science","volume-title":"The Z Notation: A Reference Manual","author":"J.M. Spivey","year":"1989","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual. International Series in Computer Science. Prentice-Hall, New York (1989) ISBN 013983768X"},{"issue":"2","key":"11_CR81","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1006\/inco.1994.1046","volume":"111","author":"J.-P. Talpin","year":"1994","unstructured":"Talpin, J.-P., Jouvelot, P.: The type and effect discipline. Information and Computation\u00a0111(2), 245\u2013296 (1994)","journal-title":"Information and Computation"},{"key":"11_CR82","volume-title":"The Object Constraint Language: Precise Modeling with UML","author":"J. Warmer","year":"1999","unstructured":"Warmer, J., Kleppe, A.: The Object Constraint Language: Precise Modeling with UML. Addison Wesley, Reading (1999)"},{"issue":"1","key":"11_CR83","first-page":"10","volume":"12","author":"J. Warmer","year":"1999","unstructured":"Warmer, J., Kleppe, A.: OCL: The constraint language of the UML. Journal of Object-Oriented Programming\u00a012(1), 10\u201313, 28 (1999)","journal-title":"Journal of Object-Oriented Programming"},{"key":"11_CR84","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/BFb0057015","volume-title":"ECOOP \u201991 European Conference on Object-Oriented Programming","author":"A. Wills","year":"1991","unstructured":"Wills, A.: Capsules and types in Fresco: Program validation in Smalltalk. In: America, P. (ed.) ECOOP 1991. LNCS, vol.\u00a0512, pp. 59\u201376. Springer, Heidelberg (1991)"},{"issue":"1","key":"11_CR85","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 Transactions on Programming Languages and Systems\u00a09(1), 1\u201324 (1987)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"11_CR86","unstructured":"Wing, J.M.: A two-tiered approach to specifying programs. Technical Report TR-299, Massachusetts Institute of Technology, Laboratory for Computer Science (1983)"},{"key":"11_CR87","unstructured":"Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice Hall International Series in Computer Science (1996)"}],"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\/978-3-540-39656-7_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T09:56:42Z","timestamp":1740218202000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39656-7_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540203032","9783540396567"],"references-count":87,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39656-7_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003]]}}}