{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:16:43Z","timestamp":1725484603121},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540431664"},{"type":"electronic","value":"9783540456483"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45648-1_4","type":"book-chapter","created":{"date-parts":[[2007,5,28]],"date-time":"2007-05-28T01:26:02Z","timestamp":1180315562000},"page":"62-81","source":"Crossref","is-referenced-by-count":3,"title":["Checking Z Data Refinements Using an Animation Tool"],"prefix":"10.1007","author":[{"given":"Neil J.","family":"Robinson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,1,22]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: assigning programs to meanings","author":"J.-R. Abrial","year":"1996","unstructured":"J.-R. Abrial. The B-book: assigning programs to meanings. Cambridge University Press, Cambridge, UK, 1996."},{"key":"4_CR2","unstructured":"M. Butler, J. Grundy, T. L\u00e5ngbacka, R. Ruk\u0161\u0117nas, and J. von Wright. The refinement calculator: Proof support for program refinement. In L. Groves and S. Reeves, editors, Formal Methods Pacific\u2019 97, pages 40\u201361. Springer-Verlag, 1997."},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"E. Clarke, O. Grumberg, and D. Long. Model-checking and abstraction. In Proc. of the 19th ACM Symposium on Principles of Programming Languages, pages 343\u2013354. ACM Press, 1992.","DOI":"10.1145\/143165.143235"},{"key":"4_CR4","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/BF01212407","volume":"5","author":"P. H. B. Gardiner","year":"1993","unstructured":"P. H. B. Gardiner and C. Morgan. A single complete rule for data refinement. Formal Aspects of Computing, 5:367\u2013382, 1993.","journal-title":"Formal Aspects of Computing"},{"key":"4_CR5","unstructured":"N. Hamilton, D. Hazel, P. Kearney, O. Traynor, and L. Wildman. A complete formal development using Cogito. In C. McDonald, editor, Computer Science\u2019 98: Proc. 21st Australasian Computer Science Conference, pages 319\u2013330. Springer-Verlag, 1998."},{"key":"4_CR6","unstructured":"I. J. Hayes. Correctness of data representations. In Proceedings of the 2nd Australian Software Engineering Conference (ASWEC-87), Canberra, pages 75\u201386. IREE (Australia), May 1987."},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"D. Hazel, P. Strooper, and O. Traynor. Possum: An animator for the Sum specification language. In W. Wong and K. Leung, editors, Proceedings Asia-Pacific Software Engineering Conference and International Computer Science Conference, pages 42\u201351. IEEE Computer Society Press, December 1997.","DOI":"10.1109\/APSEC.1997.640160"},{"key":"4_CR8","unstructured":"C. A. R. Hoare and Jifeng He. Unified Theories of Programming. Prentice Hall International Series in Computer Science, 1998."},{"issue":"2","key":"4_CR9","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/0020-0190(87)90224-9","volume":"25","author":"C. A. R. Hoare","year":"1987","unstructured":"C. A. R. Hoare, Jifeng He, and J. W. Sanders. Prespecification in data refinement. Information Processing Letters, 25(2):71\u201376, May 1987.","journal-title":"Information Processing Letters"},{"issue":"7","key":"4_CR10","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1109\/32.538605","volume":"22","author":"D. Jackson","year":"1996","unstructured":"D. Jackson and C. A. Damon. Elements of style: Analyzing a software design feature with a counterexample detector. IEEE Transactions on Software Engineering, 22(7):484\u2013495, July 1996.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"4_CR11","unstructured":"W. Johnston and L. Wildman. The Sum reference manual. Technical Report 99-21, Software Verification Research Centre, School of Information Technology, The University of Queensland, Brisbane 4072, Australia, November 1999."},{"key":"4_CR12","unstructured":"D. T. Jordan, C. J. Locke, J. A. McDermid, C. E. Parker, B. A. P. Sharp, and I. Toyn. Literate formal development of Ada from Z for safety critical applications. In Proceedings of SafeComp\u201994. ISA, 1994."},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"J. McDonald and P. Strooper. Translating Object-Z specifications to passive test oracles. In John Staples, Michael Hinchey, and Shaoying Liu, editors, Second International Conference on Formal Engineering Methods, Brisbane, Australia, December 9-11, 1998, pages 165\u2013174, 1998.","DOI":"10.1109\/ICFEM.1998.730580"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"T. Miller and P. Strooper. Animation can show only the presence of errors, never their absence. In D. D. Grant and L. Sterling, editors, Proceedings of the Australian Software Engineering Conference, ASWEC 2001, Canberra, Australia, pages 76\u201385. IEEE Computer Society Press, 2001.","DOI":"10.1109\/ASWEC.2001.948500"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"T. Miller and P. Strooper. Combining the animation and testing of abstract data types. In Proceedings of the Second Asia-Pacific Conference on Quality Software, APAQS 2001, Hong Kong. IEEE Computer Society Press, December 2001. (to appear).","DOI":"10.1109\/APAQS.2001.990027"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"N. J. Robinson and C. Fidge. Visualisation of refinements. In D. D. Grant and L. Sterling, editors, Proceedings of the Australian Software Engineering Conference, ASWEC 2001, Canberra, Australia, pages 244\u2013251. IEEE Computer Society Press, 2001.","DOI":"10.1109\/ASWEC.2001.948518"},{"key":"4_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1007\/978-3-540-49676-2_20","volume-title":"More powerful Z data refinement: Pushing the state of the art in industrial refinement","author":"S. Stepney","year":"1998","unstructured":"S. Stepney, D. Cooper, and J. Woodcock. More powerful Z data refinement: Pushing the state of the art in industrial refinement. In J. Bowen, A. Fett, and M. Hinchey, editors, ZUM\u201998: The Z Formal Specification Notation, 11th International Conference of Z Users, Lecture Notes in Computer Science, pages 284\u2013307. Springer-Verlag, 1998."},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"H. Waeselynck and S. Behnia. B model animation for external verification. In J. Staples, M. Hinchey, and S. Liu, editors, Second International Conference on Formal Engineering Methods, Brisbane, Australia, December 9-11, 1998, pages 36\u201345. IEEE Computer Society Press, 1998.","DOI":"10.1109\/ICFEM.1998.730568"},{"key":"4_CR19","unstructured":"J. Woodcock and J. Davies. Using Z: Specification, refinement, and proof. International Series in Computer Science. Prentice Hall, 1996."}],"container-title":["Lecture Notes in Computer Science","ZB 2002:Formal Specification and Development in Z and B"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45648-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T19:22:02Z","timestamp":1550344922000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45648-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540431664","9783540456483"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-45648-1_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}