{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:59:14Z","timestamp":1725544754061},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540358008"},{"type":"electronic","value":"9783540358336"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"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":[[2006]]},"DOI":"10.1007\/11786160_3","type":"book-chapter","created":{"date-parts":[[2006,7,3]],"date-time":"2006-07-03T19:40:49Z","timestamp":1151955649000},"page":"48-70","source":"Crossref","is-referenced-by-count":8,"title":["Making Specifications Complete Through Models"],"prefix":"10.1007","author":[{"given":"Bernd","family":"Schoeller","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tobias","family":"Widmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bertrand","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book \u2013 assigning programs to meanings","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book \u2013 assigning programs to meanings. Cambridge University Press, Cambridge (1996)"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Rustan, K., Leino, M., Schulte, W.: The spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"issue":"4","key":"3_CR3","first-page":"517","volume":"25","author":"M. Barnett","year":"2001","unstructured":"Barnett, M., Schulte, W.: The ABCs of specifications: AsmL, behavior, and components. Informatica\u00a025(4), 517\u2013526 (2001)","journal-title":"Informatica"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44622-2_1","volume-title":"Computer Science Logic","author":"A. Blass","year":"2000","unstructured":"Blass, A., Gurevich, Y.: Background, reserve, and gandy machines. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol.\u00a01862, pp. 1\u201317. Springer, Heidelberg (2000)"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Technical Report R0309, NIII (2003)","DOI":"10.1016\/S1571-0661(04)80810-7"},{"key":"3_CR6","first-page":"221","volume-title":"ACM Transactions on Software Engineering and Methodology","author":"Y. Cheon","year":"1994","unstructured":"Cheon, Y., Leavens, G.T.: The larch\/smalltalk interface specification language. In: ACM Transactions on Software Engineering and Methodology, vol.\u00a03, pp. 221\u2013253. ACM Press, New York (1994)"},{"key":"3_CR7","unstructured":"Cheon, Y., Leavons, G.T., Sitaraman, M., Edwards, S.: Model variables: Cleanly supporting abstraction in design by contract. Technical Report 03-10, Iowa State University (April 2003)"},{"key":"3_CR8","unstructured":"Ciupa, I., Leitner, A.: Automatic testing based on design by contract. In: Proceedings of Net.ObjectDays 2005. tranSIT Th\u00fcringer Anwendungszentrum f\u00fcr Software, Informations- und Kommunikationstechnologien GmbH (to be published, 2005)"},{"key":"3_CR9","unstructured":"Dubois, P., Howard, M., Meyer, B., Schweitzer, M., Stapf, E.: From calls to agents. Journal of Object-Oriented Programming\u00a012(6) (1999)"},{"key":"3_CR10","unstructured":"Eiffel Software. EiffelBase (August 2005), http:\/\/archive.eiffel.com\/products\/base\/"},{"issue":"1","key":"3_CR11","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1145\/343369.343384","volume":"1","author":"Y. Gurevich","year":"2000","unstructured":"Gurevich, Y.: Sequential abstract state machines capture sequential algorithms. ACM Transactions on Computational Logic\u00a01(1), 77\u2013111 (2000)","journal-title":"ACM Transactions on Computational Logic"},{"key":"3_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2704-5","volume-title":"Larch: Languages and Tools for Formal Specifications","author":"J.V. Guttag","year":"1993","unstructured":"Guttag, J.V., Jorning, J.J., Garland, S.J., Jones, K.D., Modet, A., Wing, J.M.: Larch: Languages and Tools for Formal Specifications. Springer, New York (1993)"},{"issue":"4","key":"3_CR13","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":"3_CR14","first-page":"295","volume-title":"TOOLS 1998: Proceedings of the Technology of Object-Oriented Languages and Systems","author":"R. Kramer","year":"1998","unstructured":"Kramer, R.: iContract - the Java(tm) Design by Contract(tm) tool. In: TOOLS 1998: Proceedings of the Technology of Object-Oriented Languages and Systems, p. 295. IEEE Computer Society, Washington (1998)"},{"key":"3_CR15","unstructured":"Leavens, G.T.: Larch\/C++, an interface specification language for C++. Technical report, Iowa State University, Ames, Iowa 50011 USA (August 1997)"},{"key":"3_CR16","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06t, Department of Computer Science, Iowa State University (June 1998)"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11693024_9","volume-title":"Programming Languages and Systems","author":"K.R. M. Leino","year":"2006","unstructured":"M. Leino, K.R., M\u00fcller, P.: A verification methodology for model fields. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol.\u00a03924, pp. 115\u2013130. Springer, Heidelberg (2006)"},{"issue":"9","key":"3_CR18","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/83880.84464","volume":"33","author":"B. Meyer","year":"1990","unstructured":"Meyer, B.: Tools for the new culture: Lessons from the design of the eiffel libraries. Communications of the ACM\u00a033(9), 40\u201360 (1990)","journal-title":"Communications of the ACM"},{"key":"3_CR19","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":"3_CR20","volume-title":"Reusable software: the Base object-oriented component libraries","author":"B. Meyer","year":"1994","unstructured":"Meyer, B.: Reusable software: the Base object-oriented component libraries. Prentice-Hall, Englewood Cliffs (1994)"},{"key":"3_CR21","volume-title":"Object-Oriented Software Construction","author":"B. Meyer","year":"1997","unstructured":"Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall, Englewood Cliffs (1997)","edition":"2"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-36498-6_6","volume-title":"Abstract State Machines 2003. Advances in Theory and Practice","author":"B. Meyer","year":"2003","unstructured":"Meyer, B.: A framework for proving contract-equipped classes. In: B\u00f6rger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol.\u00a02589, pp. 108\u2013125. Springer, Heidelberg (2003)"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11531142_1","volume-title":"ECOOP 2005 - Object-Oriented Programming","author":"B. Meyer","year":"2005","unstructured":"Meyer, B.: Attached types and their application to three open problems of object-oriented programming. In: Black, A.P. (ed.) ECOOP 2005. LNCS, vol.\u00a03586, pp. 1\u201332. Springer, Heidelberg (2005)"},{"key":"3_CR24","unstructured":"Meyer, B. (ed.): Eiffel Analysis, Design and Programming Language. ECMA International; As approved as International Standard 367 (June 2005)"},{"key":"3_CR25","unstructured":"Meyer, B.: Eiffel: The language, 3rd edn. (August 2005), http:\/\/se.ethz.ch\/~meyer\/ongoing\/etl\/"},{"key":"3_CR26","volume-title":"Design by Contract, by example","author":"R. Mitchell","year":"2002","unstructured":"Mitchell, R., McKim, J.: Design by Contract, by example. Addison-Wesley, Reading (2002)"},{"key":"3_CR27","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, 117\u2013154 (2003)","journal-title":"Concurrency and Computation: Practice and Experience"},{"key":"3_CR28","volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2004","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2004)"},{"key":"3_CR29","unstructured":"Nonprofit International Consortium for Eiffel (NICE). The Eiffel Library Standard, TR-EI-48\/KL (June 1995)"},{"key":"3_CR30","unstructured":"Object Management Group. UML 2.0 OCL Specification, adopted specification, ptc\/13-10-14 (November 2003)"},{"key":"3_CR31","unstructured":"Schoeller, B.: Strengthening eiffel contracts using models. In: Van, H.D., Liu, Z. (eds.) Proceeding of the Workshop on Formal Aspects of Component Software FACS 2003, number 284 in UNU\/IIST Report, pp. 143\u2013158 (September 2003)"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Spivey, J.M.: An introduction to Z and formal specifications. Software Engineering Journal (January 1989)","DOI":"10.1049\/sej.1989.0006"},{"key":"3_CR33","series-title":"International Series in Computer Science","volume-title":"The Z Notation: A Reference Manual","author":"J.M. Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1992)","edition":"2"},{"key":"3_CR34","unstructured":"Steria, Aix-en-Provence, France. Atelier B Interactive Prover User Manual"},{"key":"3_CR35","unstructured":"Widmer, T.: Reusable mathematical models. Master\u2019s thesis, ETH Z\u00fcrich (July 2004)"}],"container-title":["Lecture Notes in Computer Science","Architecting Systems with Trustworthy Components"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11786160_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,7]],"date-time":"2023-05-07T18:35:18Z","timestamp":1683484518000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11786160_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540358008","9783540358336"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/11786160_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}