{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:17:35Z","timestamp":1725455855172},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540627173"},{"type":"electronic","value":"9783540684909"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0027287","type":"book-chapter","created":{"date-parts":[[2005,11,19]],"date-time":"2005-11-19T02:00:45Z","timestamp":1132365645000},"page":"113-134","source":"Crossref","is-referenced-by-count":0,"title":["W Reconstructed"],"prefix":"10.1007","author":[{"given":"Jon","family":"Hall","sequence":"first","affiliation":[]},{"given":"Andrew","family":"Martin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,17]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Jonathan P. Bowen and Mike J. C. Gordon. Z and HOL. In J. P. Bowen and J. A. Hall, editors, Z User Workshop, Cambridge 1994, Workshops in Computing, pages 141\u2013167. Springer-Verlag, 1994.","DOI":"10.1007\/978-1-4471-3452-7_9"},{"key":"8_CR2","unstructured":"Jonathan P. Bowen and Michael G. Hinchey, editors. ZUM'95: The Z Formal Specification Notation, volume 967 of LNCS. Springer-Verlag, 1995."},{"key":"8_CR3","volume-title":"ZIP Project Technical Report ZIP\/PRG\/92\/121, SRC Document: 132, Version 1.0","author":"S. M. Brien","year":"1992","unstructured":"S. M. Brien, J. E. Nicholls, et al. Z base standard. ZIP Project Technical Report ZIP\/PRG\/92\/121, SRC Document: 132, Version 1.0, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK, November 1992."},{"key":"8_CR4","unstructured":"Stephen M. Brien. A Model and Logic for Generically Typed Set Theory (Z). D.Phil. thesis, University of Oxford, 1995. New version expected 1996."},{"key":"8_CR5","unstructured":"Marcin Engel and Jens Ulrik Skakkeeb\u00e6k. Applying PVS to Z. ProCoS II Technical Report IT\/DTU ME 3\/1, Department of Computer Science, Technical University of Denmark, December 1994."},{"key":"8_CR6","volume-title":"Technical Report WTH\/P7\/001","author":"W. T. Harwood","year":"1991","unstructured":"W. T. Harwood. Proof rules for Balzac. Technical Report WTH\/P7\/001, Imperial Software Technology, Cambridge, UK, 1991."},{"issue":"1","key":"8_CR7","first-page":"10","volume":"1","author":"R. B. Jones","year":"1992","unstructured":"R. B. Jones. ICL ProofPower. BCS FACS FACTS, Series III, 1(1):10\u201313, Winter 1992.","journal-title":"BCS FACS FACTS, Series III"},{"key":"8_CR8","unstructured":"Ina Kraan and Peter Baumann. Implementing Z in Isabelle. In Bowen and Hinchey [BH95], pages 355\u2013373."},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Kolyang, T. Santen, and B. Wolff. A structure preserving encoding of Z in Isabelle\/HOL. In 1996 International Conference on Theorem Proving in Higher Order Logic. Springer-Verlag, 1996.","DOI":"10.1007\/BFb0105411"},{"key":"8_CR10","unstructured":"Andrew Martin. Encoding W: A Logic for Z in 2OBJ. In J. C. P. Woodcock and P. G. Larsen, editors, FME'93: Industrial-Strength Formal Methods, volume 670 of Lecture Notes in Computer Science, pages 462\u2013481. Springer-Verlag, 1993."},{"issue":"4","key":"8_CR11","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1007\/BF01213535","volume":"8","author":"A. P. Martin","year":"1996","unstructured":"A. P. Martin, P. H. B. Gardiner, and J. C. P. Woodcock. A tactic calculus. Formal Aspects of Computing, 8(4):479\u2013489. Springer-Verlag, 1996.","journal-title":"Formal Aspects of Computing"},{"key":"8_CR12","unstructured":"John Nicholls, editor. Z Notation. Z Standards Panel, ISO Panel JTC1\/SC22\/ WG19 (Rapporteur Group for Z), 1995. Version 1.2, ISO Committee Draft."},{"key":"8_CR13","first-page":"223","volume-title":"Z User Workshop","author":"M. Saaltink","year":"1992","unstructured":"M. Saaltink. Z and Eves. In J. E. Nicholls, editor, Z User Workshop, York 1991, Workshops in Computing, pages 223\u2013242. Springer-Verlag, 1992."},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Graeme Smith. Extending W for Object-Z. In Bowen and Hinchey [BH95], pages 276\u2013295.","DOI":"10.1007\/3-540-60271-2_126"},{"key":"8_CR15","unstructured":"I. Toyn and J.G. Hall. Proving Conjectures using Cadi\u2124. Cadi\u2124 documentation (to appear as a York University Technical Report)."},{"issue":"3","key":"8_CR16","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1002\/spe.4380250306","volume":"25","author":"I. Toyn","year":"1991","unstructured":"I. Toyn and J.A. McDermid. Cadi\u2124: An architecture for Z tools and its implementation. Software\u2014Practice and Experience, 25(3):305\u2013330, 1991.","journal-title":"Software\u2014Practice and Experience"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"J. C. P. Woodcock and S. M. Brien. W: A Logic for Z. In Proceedings 6th Z User Meeting. Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4471-3203-5_4"}],"container-title":["Lecture Notes in Computer Science","ZUM '97: The Z Formal Specification Notation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0027287","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,10]],"date-time":"2020-04-10T21:31:35Z","timestamp":1586554295000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0027287"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540627173","9783540684909"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/bfb0027287","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}