{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,21]],"date-time":"2026-03-21T03:17:16Z","timestamp":1774063036400,"version":"3.50.1"},"publisher-location":"Boston, MA","reference-count":36,"publisher":"Springer US","isbn-type":[{"value":"9781461373834","type":"print"},{"value":"9781461552291","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/978-1-4615-5229-1_12","type":"book-chapter","created":{"date-parts":[[2013,3,11]],"date-time":"2013-03-11T00:07:08Z","timestamp":1362960428000},"page":"175-188","source":"Crossref","is-referenced-by-count":191,"title":["JML: A Notation for Detailed Design"],"prefix":"10.1007","author":[{"given":"Gary T.","family":"Leavens","sequence":"first","affiliation":[]},{"given":"Albert L.","family":"Baker","sequence":"additional","affiliation":[]},{"given":"Clyde","family":"Ruby","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","volume-title":"The Java Series","author":"K Arnold","year":"1998","unstructured":"Arnold, K. and Gosling, J. The Java Programming Language. The Java Series. Addison-Wesley, Reading, MA, second edition, 1998.","edition":"second"},{"issue":"10","key":"12_CR2","doi-asserted-by":"publisher","first-page":"785","DOI":"10.1109\/32.469460","volume":"21","author":"A Borgida","year":"1995","unstructured":"Borgida, A., Mylopoulos, J., and Reiter, R. On the frame problem in procedure specifications. IEEE Transactions on Software Engineering, 21(10):785\u2013798, October 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Dhara, K. K. and Leavens, G. T. Forcing behavioral subtyping through specification inheritance. In Proceedings of the 18th International Conference on Software Engineering, Berlin, Germany, pages 258\u2013267. IEEE Computer Society Press, March 1996. A corrected version is Iowa State University, Dept. of Computer Science TR #95-20c.","DOI":"10.1109\/ICSE.1996.493421"},{"issue":"2","key":"12_CR4","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, 22(2): 158\u2013159, February 1996.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"12_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2704-5","volume-title":"Larch: Languages and Tools for Formal Specification","author":"JV Guttag","year":"1993","unstructured":"Guttag, J. V, Horning, J. J., Garland, S., Jones, K., Modet, A., and Wing, J. Larch: Languages and Tools for Formal Specification. Springer-Verlag, New York, N.Y.,1993."},{"key":"12_CR6","volume-title":"The Java Language Specification","author":"J Gosling","year":"1996","unstructured":"Gosling, J., Joy, B., and Steele, G. The Java Language Specification. The Java Series. Addison-Wesley, Reading, MA, 1996."},{"issue":"4","key":"12_CR7","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"H C. A. R","year":"1972","unstructured":"Hoare, C. A. R. Proof of correctness of data representations. Acta Informatica, 1(4):271\u2013281, 1972.","journal-title":"Acta Informatica"},{"key":"12_CR8","unstructured":"Hayes, I., editor.Specification Case Studies. International Series in Computer Science. Prentice-Hall, Inc., second edition, 1993."},{"key":"12_CR9","volume-title":"International Series in Computer Science","author":"CB Jones","year":"1990","unstructured":"[J90]Jones, C. B. Systematic Software Development Using VDM. International Series in Computer Science. Prentice Hall, Englewood Cliffs, N.J., second edition, 1990.","edition":"second"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Kiczales, G. and Lamping, J. Issues in the design and documentation of class libraries. ACM SIGPLAN Notices, 27(10):435\u2013451, October 1992. OOPSLA\u2019 92 Proceedings, Andreas Paepcke (editor).","DOI":"10.1145\/141937.141971"},{"key":"12_CR11","unstructured":"[L91]Lerner, R. A. Specifying objects of concurrent systems. Ph.D. Thesis CMU-CS-91-131, School of Computer Science, Carnegie Mellon University, May 1991."},{"key":"12_CR12","unstructured":"Leino, K. R. 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, November 1995. Obtain from the author, at rustan@pa.dec.com."},{"key":"12_CR13","unstructured":"Leino, K. R. M. Toward Reliable Modular Programs. PhD thesis, California Institute of Technology, 1995. Available as Technical Report Caltech-CS-TR-95-03."},{"key":"12_CR14","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":"GT Leavens","year":"1996","unstructured":"Leavens, G. T. An overview of Larch\/C++: Behavioral specifications for C++ modules. In Kilov, H. and Harvey, W., editors, Specification of Behavioral Semantics in Object-Oriented Information Modeling, chapter 8, pages 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":"12_CR15","unstructured":"Leavens, G. T. Larch frequently asked questions. Version 1.89. Available in http:\/\/www.cs.iastate.edu \/~leavens\/larch-faq.html, January 1998."},{"key":"12_CR16","unstructured":"Leavens, G. T. Larch\/C++ Reference Manual. Version 5.41. 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, April 1999."},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Leavens, G. T. and Baker, A. L. Enhancing the pre-and postcondition technique for more expressive specifications. Technical Report 97-19a, Iowa State University, Department of Computer Science, February 1999.","DOI":"10.1007\/3-540-48118-4_8"},{"key":"12_CR18","unstructured":"Leavens, G. T, Baker, A. L., and Ruby, C. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06e, Iowa State University, Department of Computer Science, June 1999."},{"key":"12_CR19","volume-title":"Object-Oriented Specification Case Studies. The Object-Oriented Series","author":"K Lano","year":"1994","unstructured":"Lano, K. and Haughton, H., editors. Object-Oriented Specification Case Studies. The Object-Oriented Series. Prentice Hall, New York, N.Y., 1994."},{"issue":"6","key":"12_CR20","doi-asserted-by":"publisher","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"B Liskov","year":"1994","unstructured":"Liskov, B. and Wing, J. A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems, 16(6): 1811\u20131841, November 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"10","key":"12_CR21","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\u201c. Computer, 25(10):40\u201351, October 1992.","journal-title":"Computer"},{"key":"12_CR22","volume-title":"Eiffel: The Language. Object-Oriented Series","author":"B Meyer","year":"1992","unstructured":"Meyer, B. Eiffel: The Language. Object-Oriented Series. Prentice Hall, New York, N.Y., 1992."},{"key":"12_CR23","volume-title":"Programming from Specifications","author":"C Morgan","year":"1994","unstructured":"Morgan, C. Programming from Specifications: Second Edition. Prentice HallInternational, Hempstead, UK, 1994.","edition":"Second"},{"key":"12_CR24","volume-title":"Object-oriented Software Construction","author":"B Meyer","year":"1997","unstructured":"[M97]Meyer, B. Object-oriented Software Construction. Prentice Hall, New York, N.Y., second edition, 1997.","edition":"second"},{"issue":"4","key":"12_CR25","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/190679.190681","volume":"19","author":"WE Ogden","year":"1994","unstructured":"Ogden, W. E, Sitaraman, M., Weide, B. W, and Zweben, S. H. Part I: The RESOLVE framework and discipline \u2014 a research synopsis. ACM SIGSOFT Software Engineering Notes, 19(4):23\u201328, Oct 1994.","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"12_CR26","unstructured":"Poetzsch-Heffter, A. Specification and verification of object-oriented programs. Habilitation thesis, Technical University of Munich, January 1997."},{"key":"12_CR27","volume-title":"International Series in Computer Science","author":"JM Spivey","year":"1992","unstructured":"Spivey, J. M. The Z Notation: A Reference Manual.International Series in Computer Science.Prentice-Hall, New York, N.Y.,second edition, 1992.","edition":"second"},{"key":"12_CR28","volume-title":"Department of Computer Science","author":"G Sivaprasad","year":"1995","unstructured":"Sivaprasad, G. Larch\/CORBA: Specifying the behavior of CORBA-IDL interfaces. Technical Report 95-27a, Department of Computer Science, Iowa State University, Ames, Iowa, 50011, December 1995."},{"issue":"10","key":"12_CR29","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1145\/236337.236363","volume":"31","author":"P Steyaert","year":"1996","unstructured":"Steyaert, P., Lucas, C, Mens, K., and D\u2019Hondt, T. Reuse contracts: Managing the evolution of reusable assets. In OOPSLA\u2019 96 Conference on Object-Oriented Programming Systems, Languagges and Applications, pages 268\u2013285. ACM Press, October 1996. ACM SIGPLAN Notices, Volume 31, Number 10.","journal-title":"OOPSLA\u2019 96 Conference on Object-Oriented Programming Systems, Languagges and Applications"},{"issue":"8","key":"12_CR30","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/185087.185106","volume":"29","author":"YM Tan","year":"1994","unstructured":"Tan, Y. M. Interface language for supporting programming styles. ACM SIGPLAN Notices, 29(8):74\u201383, August 1994. Proceedings of the Workshop on Interface Definition Languages.","journal-title":"ACM SIGPLAN Notices"},{"key":"12_CR31","volume-title":"Kluwer International Series in Software Engineering","author":"YM Tan","year":"1995","unstructured":"Tan, Y. M. Formal Specification Techniques for Engineering Modular C Programs, volume 1 of Kluwer International Series in Software Engineering. Kluwer Academic Publishers, Boston, 1995."},{"key":"12_CR32","unstructured":"[W83]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":"12_CR33","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/9758.10500","volume":"9","author":"JM Wing","year":"1987","unstructured":"[W87]Wing, J. M. Writing Larch interface language specifications. ACM Transactions on Programming Languages and Systems, 9(1): 1\u201324, January 1987.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"9","key":"12_CR34","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1109\/2.58215","volume":"23","author":"JM Wing","year":"1990","unstructured":"[W90]Wing, J. M. A specifier\u2019s introduction to formal methods. Computer, 23(9):8\u201324, September 1990.","journal-title":"Computer"},{"key":"12_CR35","unstructured":"[W94]Wills, A. Refinement in Fresco. In Lano and Houghton [LH94], chapter 9, pages 184\u2013201."},{"key":"12_CR36","unstructured":"Wahls, T., Leavens, G. T, and Baker, A. L. Executing formal specifications with constraint programming. Technical Report 97-12a, Department of Computer Science, Iowa State University, 226 Atanasoff Hall, Ames, Iowa 50011, August 1998. Available by anonymous ftp from ftp.cs.iastate.edu or by e-mail from almanac @ cs.iastate.edu."}],"container-title":["Behavioral Specifications of Businesses and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4615-5229-1_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T23:44:18Z","timestamp":1745970258000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-1-4615-5229-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9781461373834","9781461552291"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-1-4615-5229-1_12","relation":{},"subject":[],"published":{"date-parts":[[1999]]}}}