{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T00:10:32Z","timestamp":1743034232108,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"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_13","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T16:12:53Z","timestamp":1183479173000},"page":"178-196","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Introducing Backward Refinement into B"],"prefix":"10.1007","author":[{"given":"Steve","family":"Dunne","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,5,27]]},"reference":[{"issue":"2","key":"13_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253\u2013284, 1991.","journal-title":"Theoretical Computer Science"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"J.-R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511624162"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"W.-P. de Roever and K. Engelhardt. Data Refinement: Model-Oriented Proof Methods and their Comparison. Number 47 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998.","DOI":"10.1017\/CBO9780511663079"},{"issue":"5","key":"13_CR4","doi-asserted-by":"publisher","first-page":"663","DOI":"10.1093\/logcom\/10.5.663","volume":"10","author":"J. Derrick","year":"2000","unstructured":"J. Derrick. A single complete refinement rule for Z. Journal of Logic and Computation, 10(5): 663\u2013675, 2000.","journal-title":"Journal of Logic and Computation"},{"key":"13_CR5","unstructured":"E.W. Dijkstra. A Discipline of Programming. Prentice-Hall International, 1976."},{"key":"13_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate Calculus and Program Semantics","author":"E.W. Dijkstra","year":"1990","unstructured":"E.W. Dijkstra and C.S. Scholten. Predicate Calculus and Program Semantics. Springer Berlin, 1990."},{"key":"13_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/3-540-45648-1_14","volume-title":"ZB2002: Formal Specification and Development in Z and B","author":"S.E. Dunne","year":"2002","unstructured":"S.E. Dunne. A theory of generalised substitutions. In D. Bert, J.P. Bowen, M.C. Henson, and K. Robinson, editors, ZB2002: Formal Specification and Development in Z and B, number 2272 in Lecture Notes in Computer Science, pages 270\u2013290. Springer-Verlag, 2002."},{"key":"13_CR8","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 Carroll Morgan. A single complete rule for data refinement. Formal Aspects of Computing, 5:367\u2013382, 1993.","journal-title":"Formal Aspects of Computing"},{"issue":"1","key":"13_CR9","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1016\/0020-0190(81)90071-5","volume":"12","author":"E.C.R. Hehner","year":"1981","unstructured":"E.C.R. Hehner. Bunch theory: a simple set theory for computer science. Information Processing Letters, 12(1):26\u201330, 1981.","journal-title":"Information Processing Letters"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Wim H. Hesselink. Programs, Recursion and Unbounded Choice. Number 27 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.","DOI":"10.1017\/CBO9780511569784"},{"issue":"10","key":"13_CR11","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10): 576\u2013583, 1969.","journal-title":"Communications of the ACM"},{"key":"13_CR12","series-title":"Lect Notes Comput Sci","first-page":"187","volume-title":"Data refinement refined","author":"C.A.R. Hoare","year":"1986","unstructured":"C.A.R. Hoare, He Jifeng, and J.W. Sanders. Data refinement refined. Number 213 in Lecture Notes in Computer Science, pages 187\u2013196. Springer-Verlag, 1986."},{"key":"13_CR13","unstructured":"C.C. Morgan. Programming from Specifications (2nd edn). Prentice Hall International, 1994."},{"key":"13_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/3-540-44525-0_7","volume-title":"ZB2000: Formal Specification and Development in B and Z","author":"K. Robinson","year":"2000","unstructured":"K. Robinson. Reconciling axiomatic and model-based specifications using the B Method. In Jonathan P. Bowen, Steve Dunne, Andy Galloway, and Steve King, editors, ZB2000: Formal Specification and Development in B and Z, number 1878 in Lecture Notes in Computer Science, pages 95\u2013106. Springer, 2000."},{"key":"13_CR15","unstructured":"Steve Schneider. The B Method: an introduction. Cornerstones of Computing. Palgrave, 2001."},{"key":"13_CR16","unstructured":"J.M. Spivey. The Z Notation: a Reference Manual (2nd edn). Prentice Hall, 1992."},{"key":"13_CR17","series-title":"Lect Notes Comput Sci","first-page":"284","volume-title":"ZUM\u2019 98: The Z Formal Specification Notation, 11th International Conference of Z Users, Berlin, September,1998, Proceedings","author":"S. Stepney","year":"1997","unstructured":"Susan Stepney, David Cooper, and Jim Woodcock. More powerful Z data refinement: pushing the state of the art in industrial refinement. In Jonathan P. Bowen, Andreas Fett, and Michael G. Hinchey, editors, ZUM\u2019 98: The Z Formal Specification Notation, 11th International Conference of Z Users, Berlin, September,1998, Proceedings, number 1493 in Lecture Notes in Computer Science, pages 284\u2013307. Springer, 1997."},{"issue":"2","key":"13_CR18","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BF01192157","volume":"31","author":"J. von Wright","year":"1994","unstructured":"J. von Wright. The lattice of data refinement. Acta Informatica, 31(2):105\u2013135, 1994.","journal-title":"Acta Informatica"},{"key":"13_CR19","unstructured":"J. Woodcock and J. Davies. Using Z: Specification, Refinement and Proof. Prentice Hall, 1996."},{"key":"13_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1007\/3-540-52513-0_18","volume-title":"VDM\u2019 90, VDM and Z \u2014 Formal Methods in Software Development, Third International Symposium of VDM Europe, Kiel, FRG, April 17\u201321, 1990, Proceedings","author":"J.C.P. Woodcock","year":"1990","unstructured":"J.C.P. Woodcock and Carroll Morgan. Refinement of state-based concurrent systems. In Dines Bj\u00f8rner, C. A. R. Hoare, and Hans Langmaack, editors, VDM\u2019 90, VDM and Z \u2014 Formal Methods in Software Development, Third International Symposium of VDM Europe, Kiel, FRG, April 17\u201321, 1990, Proceedings, number 428 in Lecture Notes in Computer Science, pages 340\u2013351. Springer, 1990."}],"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_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,18]],"date-time":"2023-01-18T20:08:25Z","timestamp":1674072505000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-44880-2_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540402534","9783540448808"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-44880-2_13","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"}}]}}