{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T19:48:13Z","timestamp":1743104893258,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540402534"},{"type":"electronic","value":"9783540448808"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44880-2_22","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T16:12:53Z","timestamp":1183479173000},"page":"359-387","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Towards Practical Proofs of Class Correctness"],"prefix":"10.1007","author":[{"given":"Bertrand","family":"Meyer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,5,27]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Mart\u00edn Abadi and Luca Cardelli: A Theory of Objects, Monographs in Computer Science, Springer-Verlag, 1996.","DOI":"10.1007\/978-1-4419-8598-9"},{"key":"22_CR2","unstructured":"Jean-Raymond Abrial, The B Book, Cambridge University Press, 1995."},{"key":"22_CR3","volume-title":"Technical Report","author":"R. Back","year":"2002","unstructured":"Ralph Back, X. Fan and Viorel Preoteasa: Reasoning about Pointers in Refinement Calculus, Technical Report, Turku Centre for Computer Science, Turku (Finland), 22 August 2002."},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Richard Bornat: Proving Pointer Programs in Hoare Logic, in Mathematics of Program Construction, Springer-Verlag, 2000, pages 102\u2013106.","DOI":"10.1007\/10722010_8"},{"key":"22_CR5","unstructured":"ClearSy [name of company, no author listed]: Web documents on Atelier B, http:\/\/www.atelierb.societe.com, last consulted December 2002."},{"key":"22_CR6","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C.A.R. Hoare","year":"1972","unstructured":"C.A.R. Hoare: Proof of Correctness of Data Representations, in Acta Informatica 1 (1972), pp. 271\u2013281. Also in C.A.R. Hoare and C. B. Jones (ed.): Essays in Computing Science, Prentice Hall International, Hemel Hempstead (U.K.), 1989, pages 103\u2013115.","journal-title":"Acta Informatica"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"C. A. R. Hoare. Procedures and parameters: An axiomatic approach. In E. Engeler, editor, Symposium on Semantics of Algorithmic Languages, volume 188 of Lecture Notes in Mathematics, pages 102\u2013116. Springer-Verlag, 1971.","DOI":"10.1007\/BFb0059696"},{"key":"22_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-48743-3_1","volume-title":"ECOOP\u2019 99 \u2014 Object-Oriented Programming","author":"C.A.R. Hoare","year":"1999","unstructured":"C.A.R. Hoare and He Jifeng: A Trace Model for Pointers, in ECOOP\u2019 99 \u2014 Object-Oriented Programming, Proceedings of 13th European Conference on Object-Oriented Programming, Lisbon, June 1999, ed. Rachid Guerraoui, Lecture Notes in Computer Science 1628, Springer-Verlag, pages 1\u201317."},{"key":"22_CR9","unstructured":"Bertrand Meyer: Introduction to the Theory of Programming Languages, Prentice Hall, 1990."},{"key":"22_CR10","unstructured":"Bertrand Meyer: Object-Oriented Software Construction, 2nd edition, Prentice Hall, 1997."},{"issue":"5","key":"22_CR11","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1109\/2.675643","volume":"31","author":"B. Meyer","year":"1998","unstructured":"Bertrand Meyer, Christine Mingins and Heinz Schmidt: Providing Trusted Components to the Industry, in Computer (IEEE), vol. 31, no. 5, May 1998, pages 104\u2013105.","journal-title":"Computer (IEEE)"},{"key":"22_CR12","unstructured":"Bertrand Meyer et al.: Trusted Components papers at se.inf.ethz.ch, last consulted December 2002."},{"key":"22_CR13","unstructured":"Bertrand Meyer: Proving Pointer Program Properties, series of columns to appear in Journal of Object Technology, draft version available at http:\/\/www.inf.ethz.ch\/~meyer\/ongoing\/references\/, last consulted January 2003."},{"key":"22_CR14","unstructured":"Bertrand Meyer: A Framework for Proving Contract-Equipped Classes, to appear in Abstract State Machines 2003 \u2014 Advances in Theory and Applications, Proc. 10th International Workshop, Taormina, Italy, March 3\u20137, 2003, eds. Egon Boerger, Angelo Gargantini, Elvinia Riccobene, Springer-Verlag 2003. Prepublication copy at http:\/\/www.inf.ethz.ch\/~meyer\/publications\/, last consulted January 2003."},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Bernhard M\u00f6ller: Calculating with Pointer Structures, in Algorithmic Languages and Calculi, Proceedings of IFIP TC2\/WG2.1 Working Conference, Le Bischenberg (France), February 1997, Chapman and Hall, 1997, pages 24\u201348.","DOI":"10.1007\/978-0-387-35264-0_2"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Joseph M. Morris, A general axiom of assignment; Assignment and linked data structures; A proof of the Schorr-Waite algorithm. In Theoretical Foundations of Programming Methodology, Proceedings of the 1981 Marktoberdorf Summer School, eds. Manfred Broy and Gunther Schmidt, Reidel 1982, pages 25\u201351.","DOI":"10.1007\/978-94-009-7893-5_5"},{"key":"22_CR17","unstructured":"John C. Reynolds: Separation Logic: A Logic for Shared mutable Data Structures, in Proceedings of 17th Annual IEEE Symposium on Logic in Computer Science, Copenhagen, July 22\u201325 2002."},{"issue":"5","key":"22_CR18","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1145\/358506.358513","volume":"25","author":"N. Suzuki","year":"1982","unstructured":"Norihisha Suzuki, Analysis of Pointer \u201cRotation\u201d, in Communications of the ACM, vol. 25, no. 5, May 1982, pages 330\u2013335.","journal-title":"Communications of the ACM"}],"container-title":["Lecture Notes in Computer Science","ZB 2003: Formal Specification and Development in Z and B"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44880-2_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,8]],"date-time":"2023-02-08T22:00:06Z","timestamp":1675893606000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-44880-2_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540402534","9783540448808"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-44880-2_22","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"27 May 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}