{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T10:16:47Z","timestamp":1770977807524,"version":"3.50.1"},"reference-count":71,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2006,5,1]],"date-time":"2006-05-01T00:00:00Z","timestamp":1146441600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2006,5]]},"abstract":"<jats:p>JML is a behavioral interface specification language tailored to Java(TM). Besides pre- and postconditions, it also allows assertions to be intermixed with Java code; these aid verification and debugging. JML is designed to be used by working software engineers; to do this it follows Eiffel in using Java expressions in assertions. JML combines this idea from Eiffel with the model-based approach to specifications, typified by VDM and Larch, which results in greater expressiveness. Other expressiveness advantages over Eiffel include quantifiers, specification-only variables, and frame conditions.This paper discusses the goals of JML, the overall approach, and describes the basic features of the language through examples. It is intended for readers who have some familiarity with both Java and behavioral specification using pre- and postconditions.<\/jats:p>","DOI":"10.1145\/1127878.1127884","type":"journal-article","created":{"date-parts":[[2006,5,8]],"date-time":"2006-05-08T22:51:53Z","timestamp":1147128713000},"page":"1-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":291,"title":["Preliminary design of JML"],"prefix":"10.1145","volume":"31","author":[{"given":"Gary T.","family":"Leavens","sequence":"first","affiliation":[{"name":"Iowa State University, Ames, Iowa"}]},{"given":"Albert L.","family":"Baker","sequence":"additional","affiliation":[{"name":"ABC Virtual Communications, Inc., IA"}]},{"given":"Clyde","family":"Ruby","sequence":"additional","affiliation":[{"name":"Iowa State University, Ames, Iowa"}]}],"member":"320","published-online":{"date-parts":[[2006,5]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Addison-Wesley","author":"Arnold Ken","year":"2000"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/34985.35007"},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","unstructured":"{Ame91} \n      \n      Pierre\n       \n      America\n    .\n      \n  \n   \n  Designing an object-oriented programming language with behavioural subtyping. In J. W. de Bakker W. P. de Roever and G. Rozenberg editors Foundations of Object-Oriented Languages REX School\/Workshop Noordwijkerhout The\n   Netherlands May\/June \n  1990 volume \n  489\n   of \n  Lecture Notes in Computer Science pages \n  60\n  --\n  90\n  . \n  Springer-Verlag New York NY 1991.]]   {Ame91} Pierre America. Designing an object-oriented programming language with behavioural subtyping. In J. W. de Bakker W. P. de Roever and G. Rozenberg editors Foundations of Object-Oriented Languages REX School\/Workshop Noordwijkerhout The Netherlands May\/June 1990 volume 489 of Lecture Notes in Computer Science pages 60--90. Springer-Verlag New York NY 1991.]]","DOI":"10.1007\/BFb0019440"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00291051"},{"issue":"7","key":"e_1_2_1_5_1","first-page":"37","article-title":"Programmers love writing tests","volume":"3","author":"Beck Kent","year":"1998","journal-title":"Java Report"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.469460"},{"key":"e_1_2_1_8_1","volume-title":"Graduate Texts in Computer Science. Springer-Verlag","author":"Back Ralph-Johan","year":"1998"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/646157.679857"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2004.3.6.a3"},{"key":"e_1_2_1_13_1","first-page":"322","volume-title":"Proceedings of the International Conference on Software Engineering Research and Practice (SERP '02)","author":"Cheon Yoonsik","year":"2002"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"{CL02b} \n      Yoonsik\n       \n      Cheon\n     and \n      \n      \n      Gary T.\n       \n      Leavens\n      \n  \n  . \n  A simple and practical approach to unit testing: The JML and JUnit way. In Boris Magnusson editor ECOOP 2002 --- Object-Oriented Programming 16th European Conference M\u00e1alaga Spain Proceedings volume \n  2374\n   of \n  Lecture Notes in Computer Science pages \n  231\n  --\n  255 Berlin June \n  2002\n  . \n  Springer-Verlag\n  .]]   {CL02b} Yoonsik Cheon and Gary T. Leavens. A simple and practical approach to unit testing: The JML and JUnit way. In Boris Magnusson editor ECOOP 2002 --- Object-Oriented Programming 16th European Conference M\u00e1alaga Spain Proceedings volume 2374 of Lecture Notes in Computer Science pages 231--255 Berlin June 2002. Springer-Verlag.]]","DOI":"10.1007\/3-540-47993-7_10"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1085130.1085150"},{"key":"e_1_2_1_16_1","volume-title":"Springer-Verlag","author":"Cohen Edward","year":"1990"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/227726.227772"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.908957"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.485225"},{"key":"e_1_2_1_20_1","unstructured":"{FL98} John Fitzgerald and Peter Gorm Larsen. Modelling Systems: Practical Tools in Software Development. Cambridge Cambridge UK 1998.]]  {FL98} John Fitzgerald and Peter Gorm Larsen. Modelling Systems: Practical Tools in Software Development. Cambridge Cambridge UK 1998.]]"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/151155"},{"key":"e_1_2_1_22_1","volume-title":"Mass.","author":"Gosling James","year":"2000"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/319838.319848"},{"key":"e_1_2_1_24_1","volume-title":"Springer-Verlag","author":"Gries David","year":"1995"},{"key":"e_1_2_1_25_1","unstructured":"{Hay93} \n      \n      I.\n       \n      Hayes editor. \n  Specification Case Studies\n  . \n  International Series in Computer Science\n  . \n  Prentice-Hall Inc. second edition 1993\n  .]]   {Hay93} I. Hayes editor. Specification Case Studies. International Series in Computer Science. Prentice-Hall Inc. second edition 1993.]]"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_2_1_28_1","volume-title":"University of Nijmegen","author":"Huisman Marieke","year":"2001"},{"key":"e_1_2_1_29_1","unstructured":"{Jon90} \n      \n      Cliff B.\n       \n      Jones\n    .\n      \n  \n   \n  Systematic Software Development Using VDM\n  . \n  International Series in Computer Science\n  . \n  Prentice Hall Englewood Cliffs N.J. second\n   edition 1990\n  .]]   {Jon90} Cliff B. Jones. Systematic Software Development Using VDM. International Series in Computer Science. Prentice Hall Englewood Cliffs N.J. second edition 1990.]]"},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"{Jon91} \n      \n      H. B. M.\n       \n      Jonkers\n    .\n      \n  \n   \n  Upgrading the pre- and postcondition technique. In S. Prehn and W. J. Toetenel editors VDM '91 Formal Software Development Methods 4th International Symposium of VDM Europe Noordwijkerhout The Netherlands Volume 1: Conference Contributions volume \n  551\n   of \n  Lecture Notes in Computer Science pages \n  428\n  --\n  456\n  . \n  Springer-Verlag New York NY October \n  1991\n  .]]   {Jon91} H. B. M. Jonkers. Upgrading the pre- and postcondition technique. In S. Prehn and W. J. Toetenel editors VDM '91 Formal Software Development Methods 4th International Symposium of VDM Europe Noordwijkerhout The Netherlands Volume 1: Conference Contributions volume 551 of Lecture Notes in Computer Science pages 428--456. Springer-Verlag New York NY October 1991.]]","DOI":"10.1007\/3-540-54834-3_26"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/286942.286973"},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"{LB99} \n      \n      Gary T.\n       \n      Leavens\n     and \n      \n      \n      Albert L.\n       \n      Baker\n      \n  \n  . \n  Enhancing the pre- and postcondition technique for more expressive specifications. In Jeannette M. Wing Jim Woodcock and Jim Davies editors FM'99 --- Formal Methods: World Congress on Formal Methods in the Development of Computing Systems Toulouse France September \n  1999 Proceedings volume \n  1709\n   of \n  Lecture Notes in Computer Science pages \n  1087\n  --\n  1106\n  . \n  Springer-Verlag 1999.]]   {LB99} Gary T. Leavens and Albert L. Baker. Enhancing the pre- and postcondition technique for more expressive specifications. In Jeannette M. Wing Jim Woodcock and Jim Davies editors FM'99 --- Formal Methods: World Congress on Formal Methods in the Development of Computing Systems Toulouse France September 1999 Proceedings volume 1709 of Lecture Notes in Computer Science pages 1087--1106. Springer-Verlag 1999.]]","DOI":"10.1007\/3-540-48118-4_8"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-5229-1_12"},{"key":"e_1_2_1_34_1","unstructured":"{Lea96} Gary T. Leavens. An overview of Larch\/C++: Behavioral specifications for C++ modules. In Haim Kilov and William Harvey editors Specification of Behavioral Semantics in Object-Oriented Information Modeling chapter 8 pages 121--142. Kluwer Academic Publishers Boston 1996. An extended version is TR #96-01d Department of Computer Science Iowa State University Ames Iowa 50011.]]  {Lea96} Gary T. Leavens. An overview of Larch\/C++: Behavioral specifications for C++ modules. In Haim Kilov and William Harvey editors Specification of Behavioral Semantics in Object-Oriented Information Modeling chapter 8 pages 121--142. Kluwer Academic Publishers Boston 1996. An extended version is TR #96-01d Department of Computer Science Iowa State University Ames Iowa 50011.]]"},{"key":"e_1_2_1_35_1","unstructured":"{Lea97} Gary T. Leavens. Larch\/C++ Reference Manual. Version 5.14. Available in ftp:\/\/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 October 1997.]]  {Lea97} Gary T. Leavens. Larch\/C++ Reference Manual. Version 5.14. Available in ftp:\/\/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 October 1997.]]"},{"key":"e_1_2_1_36_1","unstructured":"{Lea00} Gary T. Leavens. Larch frequently asked questions. Version 1.110. Available in http:\/\/www.cs.iastate.edu\/~leavens\/larch-faq.html May 2000.]]  {Lea00} Gary T. Leavens. Larch frequently asked questions. Version 1.110. Available in http:\/\/www.cs.iastate.edu\/~leavens\/larch-faq.html May 2000.]]"},{"key":"e_1_2_1_38_1","volume-title":"California Institute of Technology","author":"Leino K. Rustan M.","year":"1995"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/286942.286953"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73564"},{"key":"e_1_2_1_41_1","volume-title":"Object-Oriented Specification Case Studies. The Object-Oriented Series","author":"Lano K.","year":"1994"},{"key":"e_1_2_1_42_1","volume-title":"Compaq Systems Research Center","author":"Leino K. Rustan M.","year":"2000"},{"key":"e_1_2_1_43_1","unstructured":"{LPC+05} Gary T. Leavens Erik Poll Curtis Clifton Yoonsik Cheon Clyde Ruby David R. Cok Peter M\u00fcller and Joseph Kiniry. JML reference manual. Department of Computer Science Iowa State University. Available from http:\/\/www.jmlspecs.org July 2005.]]  {LPC+05} Gary T. Leavens Erik Poll Curtis Clifton Yoonsik Cheon Clyde Ruby David R. Cok Peter M\u00fcller and Joseph Kiniry. JML reference manual. Department of Computer Science Iowa State University. Available from http:\/\/www.jmlspecs.org July 2005.]]"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512559"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.1985.230345"},{"key":"e_1_2_1_47_1","unstructured":"{LvHKBO87} \n      \n      David\n       \n      Luckham Friedrich W.\n       \n      von Henke Bernd\n       \n      Krieg-Br\u00fcckner and \n      \n      \n      Olaf\n       \n      Owe\n    .\n      \n  \n   \n  ANNA - A Language for Annotating Ada Programs volume \n  260\n   of \n  Lecture Notes in Computer Science\n  . \n  Springer-Verlag New York NY 1987\n  .]]   {LvHKBO87} David Luckham Friedrich W. von Henke Bernd Krieg-Br\u00fcckner and Olaf Owe. ANNA - A Language for Annotating Ada Programs volume 260 of Lecture Notes in Computer Science. Springer-Verlag New York NY 1987.]]"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01178658"},{"key":"e_1_2_1_50_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"520","DOI":"10.1007\/BFb0030623","volume-title":"7th International Joint Conference CAAP\/FASE","author":"Leavens Gary T.","year":"1997"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_2_1_52_1","volume-title":"Object-Oriented Series","author":"Meyer Bertrand","year":"1992"},{"key":"e_1_2_1_53_1","unstructured":"{Mey97} Bertrand Meyer. Object-oriented Software Construction. Prentice Hall New York NY second edition 1997.]]   {Mey97} Bertrand Meyer. Object-oriented Software Construction. Prentice Hall New York NY second edition 1997.]]"},{"key":"e_1_2_1_54_1","volume-title":"Prentice Hall International","author":"Morgan Carroll","year":"1994"},{"key":"e_1_2_1_55_1","unstructured":"{M\u00fcl02} \n      \n      Peter\n       \n      M\u00fcller\n    .\n      \n  \n   \n  Modular Specification and Verification of Object-Oriented Programs volume \n  2262\n   of \n  Lecture Notes in Computer Science\n  . \n  Springer-Verlag 2002\n  . The author's Ph.D. Thesis. Available from http:\/\/www.informatik.fernuni-hagen. de\/import\/pi5\/publications.html.]]  {M\u00fcl02} Peter M\u00fcller. Modular Specification and Verification of Object-Oriented Programs volume 2262 of Lecture Notes in Computer Science. Springer-Verlag 2002. The author's Ph.D. Thesis. Available from http:\/\/www.informatik.fernuni-hagen. de\/import\/pi5\/publications.html.]]"},{"key":"e_1_2_1_56_1","volume-title":"Springer-Verlag","author":"Morgan Carroll","year":"1994"},{"key":"e_1_2_1_57_1","volume-title":"Proceedings of the Fifth LOMAPS Workshop, number 1192 in Lecture Notes in Computer Science. Springer-Verlag","author":"Nielson H. R.","year":"1997"},{"key":"e_1_2_1_58_1","unstructured":"{Org96} International Standards Organization. Information technology -- programming languages their environments and system software interfaces -- Vienna Development Method -- specification language -- part 1: Base language. ISO\/IEC 13817-1 December 1996.]]  {Org96} International Standards Organization. Information technology -- programming languages their environments and system software interfaces -- Vienna Development Method -- specification language -- part 1: Base language. ISO\/IEC 13817-1 December 1996.]]"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.345827"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/190679.190681"},{"key":"e_1_2_1_61_1","volume-title":"Technical University of Munich","author":"Poetzsch-Heffter Arnd","year":"1997"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/11531142_24"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/354222.353186"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.341844"},{"key":"e_1_2_1_66_1","unstructured":"{Spi92} \n      \n      J. Michael\n       \n      Spivey\n    .\n      \n  \n   \n  The Z Notation: A Reference Manual\n  . \n  International Series in Computer Science\n  . \n  Prentice-Hall New York NY second\n   edition 1992\n  .]]   {Spi92} J. Michael Spivey. The Z Notation: A Reference Manual. International Series in Computer Science. Prentice-Hall New York NY second edition 1992.]]"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_14"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/185087.185106"},{"key":"e_1_2_1_69_1","unstructured":"{Tan95} \n      \n      Yang Meng\n       \n      Tan\n    .\n      \n  \n   \n  Formal Specification Techniques for Engineering Modular C Programs volume \n  1\n   of \n  Kluwer International Series in Software Engineering\n  . \n  Kluwer Academic Publishers Boston 1995\n  .]]   {Tan95} Yang Meng Tan. Formal Specification Techniques for Engineering Modular C Programs volume 1 of Kluwer International Series in Software Engineering. Kluwer Academic Publishers Boston 1995.]]"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1046"},{"key":"e_1_2_1_71_1","volume-title":"Prentice Hall International Series in Computer Science","author":"Woodcock Jim","year":"1996"},{"key":"e_1_2_1_72_1","first-page":"184","volume-title":"Lano and Houghton {LH94}","author":"Wills Alan"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/9758.10500"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.58215"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1026554217992"},{"key":"e_1_2_1_77_1","unstructured":"{WR25} A. N. Whitehead and B. Russell. Principia Mathematica. Cambridge University Press London second edition. edition 1925.]]  {WR25} A. N. Whitehead and B. Russell. Principia Mathematica. Cambridge University Press London second edition. edition 1925.]]"},{"key":"e_1_2_1_78_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"473","DOI":"10.1007\/3-540-55253-7_28","volume-title":"4th European Symposium on Programming","author":"Wright Andrew K.","year":"1992"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1127878.1127884","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1127878.1127884","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:18:54Z","timestamp":1750263534000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1127878.1127884"}},"subtitle":["a behavioral interface specification language for java"],"short-title":[],"issued":{"date-parts":[[2006,5]]},"references-count":71,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2006,5]]}},"alternative-id":["10.1145\/1127878.1127884"],"URL":"https:\/\/doi.org\/10.1145\/1127878.1127884","relation":{},"ISSN":["0163-5948"],"issn-type":[{"value":"0163-5948","type":"print"}],"subject":[],"published":{"date-parts":[[2006,5]]},"assertion":[{"value":"2006-05-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}