{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,26]],"date-time":"2026-10-26T17:59:49Z","timestamp":1793037589988,"version":"4.5.0"},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540437598","type":"print"},{"value":"9783540479932","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-47993-7_10","type":"book-chapter","created":{"date-parts":[[2007,5,15]],"date-time":"2007-05-15T01:12:20Z","timestamp":1179191540000},"page":"231-255","source":"Crossref","is-referenced-by-count":111,"title":["A Simple and Practical Approach to Unit Testing: The JML and JUnit Way"],"prefix":"10.1007","author":[{"given":"Yoonsik","family":"Cheon","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gary T.","family":"Leavens","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2002,5,29]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Karine Arnout and Raphael Simon. The.NET contract wizard: Adding design by contract to languages other than Eiffel. In Proceedings of TOOLS 39, 29 July\u20133 August 2001, Santa Barbara, California, pages 14\u201323. IEEE Computer Society, 2001.","DOI":"10.1109\/TOOLS.2001.941655"},{"key":"10_CR2","unstructured":"D. Bartetzko, C. Fischer, M. Moller, and H. Wehrheim. Jass-Java with assertions. In Workshop on Runtime Verification held in conjunction with the 13th Conference on Computer Aided Verification, CAV\u201901, 2001."},{"key":"10_CR3","unstructured":"Kent Beck and Erich Gamma. Test infected: Programmers love writing tests. Java Report, 3(7), July 1998."},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Kent Beck. Extreme Programming Explained. Addison-Wesley, 2000.","DOI":"10.1109\/TOOLS.1999.779100"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Gilles Bernot, Marie Claude Claudel, and Bruno Marre. Software testing based on formal specifications: a theory and a tool. Software Engineering Journal, 6(6):387\u2013405, November 1991.","DOI":"10.1049\/sej.1991.0040"},{"key":"10_CR6","volume-title":"Technical Report TR #00-08","author":"A. Bhorkar","year":"2000","unstructured":"Abhay Bhorkar. A run-time assertion checker for Java using JML. Technical Report TR #00-08, Department of Computer Science; Iowa State University, Ames, IA, May 2000."},{"key":"10_CR7","unstructured":"Manuela Carrillo-Castellon, Jesus Garcia-Molina, Ernesto Pimentel, and Israel Repiso. Design by contract in Smalltalk. Journal of Object-Oriented Programming, 9(7):23\u201328, November\/December 1996."},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Juei Chang, Debra J. Richardson, and Sriram Sankar. Structural specification-based testing with ADL. In Proceedings of ISSTA 96, San Diego, CA, pages 62\u201370. IEEE Computer Society, 1996.","DOI":"10.1145\/229000.226302"},{"key":"10_CR9","unstructured":"Yoonsik Cheon and Gary T. Leavens. A runtime assertion checker for the Java Modeling Language (JML). Technical Report 02-05, Department of Computer Science, Iowa State University, March 2002."},{"issue":"3","key":"10_CR10","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1145\/226295.226303","volume":"21","author":"J. L. Crowley","year":"1996","unstructured":"J. L. Crowley, J. F. Leathrum, and K. A. Liburdy. Isues in the full scale use of formal methods for automated testing. ACM SIGSOFT Software Engineering Notes, 21(3):71\u201378, May 1996.","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"10_CR11","unstructured":"David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. Extended static checking. SRC Research Report 159, Compaq Systems Research Center, 130 Lytton Ave., Palo Alto, Dec 1998."},{"key":"10_CR12","first-page":"99","volume-title":"USENIX C++ Technical Conference Proceedings","author":"C. K. Duby","year":"1992","unstructured":"Carolyn K. Duby, Scott Meyers, and Steven P. Reiss. CCEL: A metalanguage for C++. In USENIX C++ Technical Conference Proceedings, pages 99\u2013115, Portland, OR, August 1992. U ENIX Assoc. Berkeley, CA, USA."},{"key":"10_CR13","volume-title":"Technical Report TRCS98-32","author":"A. Duncan","year":"1998","unstructured":"Andrew Duncan and Urs Holzle. Adding contracts to Java with Handshake. Technical Report TRCS98-32, Department of Computer Science, University of California, Santa Barbara, CA, December 1998."},{"key":"10_CR14","volume-title":"Technical Report CS TR00-366","author":"R. B. Findler","year":"2000","unstructured":"Robert Bruce Findler and Matthias Felleisen. Behavioral interface contracts for Java. Technical Report CS TR00-366, Department of Computer Science, Rice University, Houston, TX, August 2000."},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Pedro Guerreiro. Simple support for design by contract in C++. In Proceedings of TOOLS 39, 29 July\u20133 August 2001, Santa Barbara, California, pages 24\u201334. IEEE Computer Society, 2001.","DOI":"10.1109\/TOOLS.2001.941656"},{"issue":"4","key":"10_CR16","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/TSE.1977.231145","volume":"3","author":"R. G. Hamlet","year":"1977","unstructured":"R. G. Hamlet. Testing programs with the aid of a compiler. IEEE Transactions on Software Engineering, 3(4):279\u2013290, July 1977.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1","key":"10_CR17","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1109\/32.263753","volume":"20","author":"Teruo Higashino and Gregor v. Bochmann","year":"1994","unstructured":"Teruo Higashino and Gregor v. Bochmann. Automatic analysis and test case derivation for a restricted class of LOTOS expressions with data parameters. IEEE Transactions on Software Engineering, 20(1):29\u201342, January 1994.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-45314-8_21","volume-title":"Fundamental Approaches to Software Engineering (FASE\u20192001), Genova, Italy, 2001","author":"B. Jacobs","year":"2001","unstructured":"Bart Jacobs and Eric Poll. A logic for the Java modeling language JML. In Fundamental Approaches to Software Engineering (FASE\u20192001), Genova, Italy, 2001, volume 2029 of Lecture Notes in Computer Science, pages 284\u2013299. Springer-Verlag, 2001."},{"issue":"1","key":"10_CR19","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/0096-0551(92)90024-H","volume":"17","author":"P. Jalote","year":"1992","unstructured":"Pankaj Jalote. Specification and testing of abstract data types. Computing Languages, 17(1):75\u201382, 1992.","journal-title":"Computing Languages"},{"key":"10_CR20","unstructured":"JUnit. http:\/\/www.junit.org ."},{"key":"10_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/3-540-48443-4_18","volume-title":"Meta-Level Architectures and Reflection, Second International Conference on Reflection\u2019 99, Saint-Malo, France, July 19\u201321, 1999, Proceedings","author":"M. Karaorman","year":"1999","unstructured":"Murat Karaorman, Urs Holzle, and John Bruno. jContractor: A reflective Java library to support design by contract. In Pierre Cointe, editor, Meta-Level Architectures and Reflection, Second International Conference on Reflection\u2019 99, Saint-Malo, France, July 19\u201321, 1999, Proceedings, volume 1616 of Lecture Notes in Computer Science, pages 175\u2013196. Springer-Verlag, July 1999."},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Bogdan Korel and Ali M. Al-Yami. Automated regression test generation. In Proceedings of ISSTA 98, Clearwater Beach, FL, pages 143\u2013152. IEEE Computer Society, 1998.","DOI":"10.1145\/271771.271803"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Reto Kramer. iContract-the Java design by contract tool. TOOLS 26: Technology of Object-Oriented Kanguages and Systems, Los Alamitos, California, pages 295\u2013307, 1998.","DOI":"10.1109\/TOOLS.1998.711021"},{"key":"10_CR24","unstructured":"Gary T. Leavens, Albert L. Baker, and Clyde Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98\u201306p, Iowa State University, Department of Computer Science, August 2001. See http:\/\/www.jmlspecs.org ."},{"key":"10_CR25","doi-asserted-by":"crossref","unstructured":"Gary T. Leavens, Albert L. Baker, and Clye Ruby. JML: A notation for detailed design. In Haim Kilov, Bernhard Rumpe, and Ian Simmonds, editors, Behavioral Specifications of Businesses and Systems, chapter 12, pages 175\u2013188. Kluwer, 1999.","DOI":"10.1007\/978-1-4615-5229-1_12"},{"key":"10_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"1087","DOI":"10.1007\/3-540-48118-4_8","volume-title":"FM\u201999-Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 1999. Proceedings","author":"G. T. Leavens","year":"1999","unstructured":"Gary T. Leavens and Albert L. Baker. Enhancing the pre-and postcondition technique for more expressive specifications. In J. Davies J.M. Wing, J. Woodcock, editor, FM\u201999-Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 1999. Proceedings, Volume II, volume 1708 of Lecture Notes in Computer Science, pages 1087\u20131106. Springer-Verlag, September 1999."},{"key":"10_CR27","series-title":"Object-Oriented Series","volume-title":"Eiffel: The Language","author":"B. Meyer","year":"1992","unstructured":"Bertrand Meyer. Eiffel: The Language. Object-Oriented Series. Prentice Hall, New York, N.Y., 1992."},{"key":"10_CR28","volume-title":"Object-oriented Software Construction","author":"B. Meyer","year":"1997","unstructured":"Bertrand Meyer. Object-oriented Software Construction. Prentice Hall, New York, N.Y., second edition, 1997.","edition":"second edition"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"B. Meyer. Applying design by contract. IEEE Computer, 25(10):40\u201351, October 1992.","DOI":"10.1109\/2.161279"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"D.J. Panzl. Automatic software test driver. IEEE Computer, pages 44\u201350, April 1978.","DOI":"10.1109\/C-M.1978.218138"},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"Dennis Peters and David L. Parnas. Generating a test oracle from program documentation. In Proceedings of ISSTA 94, Seattle, Washington, August, 1994, pages 58\u201365. IEEE Computer Society, August 1994.","DOI":"10.1145\/186258.186508"},{"key":"10_CR32","doi-asserted-by":"crossref","unstructured":"Reinhold Plosch and Josef Pichler. Contracts: From analysis to C++ implementation. In Proceedings of TOOLS 30, pages 248\u2013257. IEEE Computer Society, 1999.","DOI":"10.1109\/TOOLS.1999.787553"},{"issue":"2","key":"10_CR33","first-page":"30","volume":"8","author":"Sara Porat","year":"1995","unstructured":"Sara Porat and Paul Fertig. Class assertions in C++. Journal of Object-Oriented Programming, 8(2):30\u201337, May 1995.","journal-title":"Journal of Object-Oriented Programming"},{"key":"10_CR34","doi-asserted-by":"crossref","unstructured":"Debra J. Richardson. TAOS: Testing with analysis and oracle support. In Proceedings of ISSTA 94, Seattle, Washington, August, 1994, pages 138\u2013152. IEEE Computer Society, August 1994.","DOI":"10.1145\/186258.187158"},{"key":"10_CR35","doi-asserted-by":"crossref","unstructured":"David R. Rosenblum. A practical approach to programming with assertions. IEEE Transactions on Software Engineering, 21(1):19\u201331, January 1995.","DOI":"10.1109\/32.341844"},{"key":"10_CR36","doi-asserted-by":"crossref","unstructured":"Sriram Sankar and Roger Hayes. ADL: An interface definition language for specifying and testing software. ACM SIGPLAN Notices, 29(8):13\u201321, August 1994. Proceedings of the Workshop on Interface Definition Language, Jeannette M. Wing (editor), Portland, Oregon.","DOI":"10.1145\/185087.185096"},{"key":"10_CR37","doi-asserted-by":"crossref","unstructured":"P. Stocks and D. Carrington. Test template framework: A specification-based test case study. In Proceedings of the 1993 International Symposium on Software Testing and Analysis (ISSTA), pages 11\u201318. IEEE Computer Society, June 1993.","DOI":"10.1145\/154183.154190"},{"key":"10_CR38","unstructured":"David Welch and Scott Strong. An exception-based assertion mechanism for C++. Journal of Object-Oriented Programming, 11(4):50\u201360, July\/August 1998."}],"container-title":["Lecture Notes in Computer Science","ECOOP 2002 \u2014 Object-Oriented Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-47993-7_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T03:19:15Z","timestamp":1736997555000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-47993-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540437598","9783540479932"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/3-540-47993-7_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002]]}}}