{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T16:51:49Z","timestamp":1761929509541},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642150562"},{"type":"electronic","value":"9783642150579"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15057-9_9","type":"book-chapter","created":{"date-parts":[[2010,8,11]],"date-time":"2010-08-11T07:01:15Z","timestamp":1281510075000},"page":"127-141","source":"Crossref","is-referenced-by-count":13,"title":["Specifying Reusable Components"],"prefix":"10.1007","author":[{"given":"Nadia","family":"Polikarpova","sequence":"first","affiliation":[]},{"given":"Carlo A.","family":"Furia","sequence":"additional","affiliation":[]},{"given":"Bertrand","family":"Meyer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-book. Cambridge University Press, Cambridge (1996)"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-540-69149-5_16","volume-title":"Verified Software: Theories, Tools, Experiments","author":"M. Barnett","year":"2008","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Jacobs, B., Leino, K.R.M., Schulte, W., Venter, H.: The Spec# programming system: Challenges and directions. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol.\u00a04171, pp. 144\u2013152. Springer, Heidelberg (2008)"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Chalin, P.: Are practitioners writing contracts? In: Rigorous Development of Complex Fault-Tolerant Systems, pp. 100\u2013113 (2006)","DOI":"10.1007\/11916246_5"},{"key":"9_CR4","unstructured":"http:\/\/freeelks.svn.sourceforge.net"},{"key":"9_CR5","first-page":"80","volume-title":"Current Trends in Programming Methodology","author":"J.A. Gougen","year":"1978","unstructured":"Gougen, J.A., Thatcher, J.W., Wagner, E.G.: An initial algebra approach to the specification, correctness, and implementation of abstract data types. In: Current Trends in Programming Methodology, pp. 80\u2013149. Prentice-Hall, Englewood Cliffs (1978)"},{"key":"9_CR6","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/BF00260922","volume":"10","author":"J.V. Guttag","year":"1978","unstructured":"Guttag, J.V., Horning, J.J.: The algebraic specification of abstract data types. Acta Inf.\u00a010, 27\u201352 (1978)","journal-title":"Acta Inf."},{"key":"9_CR7","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 Inf.\u00a01, 271\u2013281 (1972)","journal-title":"Acta Inf."},{"issue":"1-3","key":"9_CR8","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. Sci. Comput. Program.\u00a055(1-3), 185\u2013208 (2005)","journal-title":"Sci. Comput. Program."},{"key":"9_CR9","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"},{"issue":"9","key":"9_CR10","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1109\/MC.2009.296","volume":"42","author":"B. Meyer","year":"2009","unstructured":"Meyer, B., Fiva, A., Ciupa, I., Leitner, A., Wei, Y., Stapf, E.: Programs that test themselves. Computer\u00a042(9), 46\u201355 (2009)","journal-title":"Computer"},{"key":"9_CR11","unstructured":"Polikarpova, N., Furia, C.A., Meyer, B.: Specifying reusable components, Extended version, http:\/\/arxiv.org\/abs\/1003.5777"},{"key":"9_CR12","unstructured":"Schoeller, B.: Making classes provable through contracts, models and frames. PhD thesis, ETH Zurich (2007)"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Schoeller, B., Widmer, T., Meyer, B.: Making specifications complete through models. In: Architecting Systems with Trustworthy Components, pp. 48\u201370 (2004)","DOI":"10.1007\/11786160_3"},{"key":"9_CR14","unstructured":"http:\/\/vsr.sourceforge.net\/"},{"key":"9_CR15","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1145\/1375581.1375624","volume-title":"PLDI 2008","author":"K. Zee","year":"2008","unstructured":"Zee, K., Kuncak, V., Rinard, M.C.: Full functional verification of linked data structures. In: PLDI 2008, pp. 349\u2013361. ACM, New York (2008)"}],"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-642-15057-9_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T03:01:01Z","timestamp":1606186861000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15057-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642150562","9783642150579"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15057-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}