{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:08:26Z","timestamp":1725516506213},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540691471"},{"type":"electronic","value":"9783540691495"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-69149-5_15","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T12:07:43Z","timestamp":1218542863000},"page":"134-143","source":"Crossref","is-referenced-by-count":4,"title":["Lessons from the JML Project"],"prefix":"10.1007","author":[{"given":"Gary T.","family":"Leavens","sequence":"first","affiliation":[]},{"given":"Curtis","family":"Clifton","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"15_CR1","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/602382.602403","volume":"50","author":"T. Hoare","year":"2003","unstructured":"Hoare, T.: The verifying compiler: A grand challenge for computing research. Journal of the ACM\u00a050(1), 63\u201369 (2003)","journal-title":"Journal of the ACM"},{"issue":"3","key":"15_CR2","doi-asserted-by":"publisher","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.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Journal on Software Tools for Technology Transfer\u00a07(3), 212\u2013232 (2005)","journal-title":"Journal on Software Tools for Technology Transfer"},{"issue":"1-3","key":"15_CR3","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-3), 185\u2013208 (2005)","journal-title":"Science of Computer Programming"},{"key":"15_CR4","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., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI 2002), June 2002. SIGPLAN, vol.\u00a037(5), pp. 234\u2013245. ACM Press, New York (2002)"},{"key":"15_CR5","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":"15_CR6","series-title":"A corrected version is ISU CS TR #95-20c","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, March 1996. A corrected version is ISU CS TR #95-20c, pp. 258\u2013267. IEEE Computer Society Press, Berlin (1996), http:\/\/tinyurl.com\/s2krg"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/11901433_2","volume-title":"Formal Methods and Software Engineering","author":"G.T. Leavens","year":"2006","unstructured":"Leavens, G.T.: JML\u2019s rich, inherited specifications for behavioral subtypes. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 2\u201334. Springer, Heidelberg (2006)"},{"unstructured":"Leavens, G.T., Naumann, D.A.: Behavioral subtyping, specification inheritance, and modular reasoning. Technical Report 06-20b, Department of Computer Science, Iowa State University, Ames, Iowa, 50011 (September 2006)","key":"15_CR8"},{"unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D.R., M\u00fcller, P., Kiniry, J., Chalin, P.: JML reference manual. In: Department of Computer Science, Iowa State University (February 2007), http:\/\/www.jmlspecs.org","key":"15_CR9"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/11766155_23","volume-title":"Emerging Trends in Information and Communication Security","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Naumann, D.A., Schulte, W., Sun, Q.: Allowing state changes in specifications. In: M\u00fcller, G. (ed.) ETRICS 2006. LNCS, vol.\u00a03995, pp. 321\u2013336. Springer, Heidelberg (2006)"},{"key":"15_CR11","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)"},{"issue":"6","key":"15_CR12","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":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-24851-4_22","volume-title":"ECOOP 2004 \u2013 Object-Oriented Programming","author":"K.R.M. Leino","year":"2004","unstructured":"Leino, K.R.M., M\u00fcller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol.\u00a03086, pp. 491\u2013516. Springer, Heidelberg (2004)"},{"issue":"5","key":"15_CR14","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1145\/570886.570888","volume":"24","author":"K.R.M. Leino","year":"2002","unstructured":"Leino, K.R.M., Nelson, G.: Data abstraction and information hiding. ACM Transactions on Programming Languages and Systems\u00a024(5), 491\u2013553 (2002)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"15_CR15","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 and Computation: Practice and Experience\u00a015(2), 117\u2013154 (2003)","journal-title":"Concurrency and Computation: Practice and Experience"},{"issue":"3","key":"15_CR16","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/j.scico.2006.03.001","volume":"62","author":"P. M\u00fcller","year":"2006","unstructured":"M\u00fcller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Science of Computer Programming\u00a062(3), 253\u2013286 (2006)","journal-title":"Science of Computer Programming"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45337-7_1","volume-title":"ECOOP 2001 - Object-Oriented Programming","author":"J. Boyland","year":"2001","unstructured":"Boyland, J., Noble, J., Retert, W.: Capabilities for sharing. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol.\u00a02072, pp. 1\u201327. Springer, Heidelberg (2001)"},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/BFb0054091","volume-title":"ECOOP \u201998 - 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)"},{"issue":"8","key":"15_CR19","doi-asserted-by":"publisher","first-page":"5","DOI":"10.5381\/jot.2005.4.8.a1","volume":"4","author":"W. Dietl","year":"2005","unstructured":"Dietl, W., M\u00fcller, P.: Universes: Lightweight ownership for JML. Journal of Object Technology\u00a04(8), 5\u201332 (2005)","journal-title":"Journal of Object Technology"},{"key":"15_CR20","volume-title":"Component Software: Beyond Object-Oriented Programming","author":"C. Szyperski","year":"2002","unstructured":"Szyperski, C., Gruntz, D., Murer, S.: Component Software: Beyond Object-Oriented Programming, 2nd edn. ACM Press and Addison-Wesley, New York (2002)","edition":"2"},{"issue":"2","key":"15_CR21","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF00264436","volume":"18","author":"G.W. Ernst","year":"1982","unstructured":"Ernst, G.W., Navlakha, J.K., Ogden, W.F.: Verification of programs with procedure-type parameters. Acta Informatica\u00a018(2), 149\u2013169 (1982)","journal-title":"Acta Informatica"},{"issue":"5","key":"15_CR22","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1109\/TSE.1984.5010277","volume":"SE-10","author":"J.A. Goguen","year":"1984","unstructured":"Goguen, J.A.: Parameterized programming. IEEE Transactions on Software Engineering\u00a0SE-10(5), 528\u2013543 (1984)","journal-title":"IEEE Transactions on Software Engineering"},{"unstructured":"B\u00fcchi, M., Weck, W.: A plea for grey-box components. Technical Report 122, Turku Center for Computer Science, Presented at the Workshop on Foundations of Component-Based Systems, Z\u00fcrich (1997) (September 1997), http:\/\/tinyurl.com\/2833tr","key":"15_CR23"},{"unstructured":"B\u00fcchi, M., Weck, W.: The greybox approach: When blackbox specifications hide too much. Technical Report 297, Turku Center for Computer Science (August (1999), http:\/\/tinyurl.com\/ywmuzy","key":"15_CR24"},{"unstructured":"B\u00fcchi, M.: Safe language mechanisms for modularization and concurrency. Technical Report TUCS Dissertations No. 28, Turku Center for Computer Science (May 2000)","key":"15_CR25"},{"unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: Debugging system software via static analysis. In: Conference Record of POPL 2002: The 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, January 16\u201318, 2002, pp. 1\u20133 (2002)","key":"15_CR26"},{"key":"15_CR27","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, New York (1992)"},{"key":"15_CR28","doi-asserted-by":"crossref","first-page":"439","DOI":"10.1145\/337180.337234","volume-title":"Proceedings of the 22nd International Conference on Software Engineering","author":"J.C. Corbett","year":"2000","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, Z.H.: Bandera: Extracting finite-state models from Java source code. In: Proceedings of the 22nd International Conference on Software Engineering, June 2000, pp. 439\u2013448. ACM Press, New York (2000)"},{"issue":"3","key":"15_CR29","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming\u00a08(3), 231\u2013274 (1987)","journal-title":"Science of Computer Programming"},{"key":"15_CR30","first-page":"511","volume-title":"Proceedings of the 2005 International Conference on Software Engineering Research and Practice (SERP 2005)","author":"Y. Cheon","year":"2005","unstructured":"Cheon, Y., Perumendla, A.: Specifying and checking method call sequences in JML. In: Arabnia, H.R., Reza, H. (eds.) Proceedings of the 2005 International Conference on Software Engineering Research and Practice (SERP 2005), June 27-29, 2005, vol.\u00a0II, pp. 511\u2013516. CSREA Press, Las Vegas, Nevada (2005)"},{"key":"15_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/11531142_24","volume-title":"ECOOP 2005 - Object-Oriented Programming","author":"E. Rodr\u00edguez","year":"2005","unstructured":"Rodr\u00edguez, E., Dwyer, M.B., Flanagan, C., Hatcliff, J., Leavens, G.T.: Robby: Extending JML for modular specification and verification of multi-threaded programs. In: Black, A.P. (ed.) ECOOP 2005. LNCS, vol.\u00a03586, pp. 551\u2013576. Springer, Heidelberg (2005)"},{"key":"15_CR32","doi-asserted-by":"publisher","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., Jones, K., Modet, A., Wing, J.: Larch: Languages and Tools for Formal Specification. Springer, New York (1993)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69149-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,19]],"date-time":"2023-05-19T10:44:10Z","timestamp":1684493050000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}