{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T05:17:34Z","timestamp":1737091054799,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439288"},{"type":"electronic","value":"9783540456148"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45614-7_26","type":"book-chapter","created":{"date-parts":[[2007,5,17]],"date-time":"2007-05-17T04:45:28Z","timestamp":1179377128000},"page":"451-470","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":28,"title":["Refinement in Circus"],"prefix":"10.1007","author":[{"given":"Augusto","family":"Sampaio","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jim","family":"Woodcock","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"26_CR1","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the Summer School on Program Design Calculi","author":"R. J. R. Back","year":"1992","unstructured":"R. J. R. Back. Refinement of parallel and reactive programs. In Proceedings of the Summer School on Program Design Calculi, Lecture Notes in Computer Science. Springer-Verlag, 1992."},{"issue":"3","key":"26_CR2","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/s001650050016","volume":"10","author":"A. L. C. Cavalcanti","year":"1999","unstructured":"A. L. C. Cavalcanti and J. C. P. Woodcock. ZRC-A Refinement Calculus for Z. Formal Aspects of Computing, 10(3):267\u2013289, 1999.","journal-title":"Formal Aspects of Computing"},{"key":"26_CR3","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E. W. Dijkstra","year":"1975","unstructured":"E. W. Dijkstra. Guarded commands, nondeterminacy and the formal derivation of programs. Communication of the ACM, 18:453\u2013457, 1975.","journal-title":"Communication of the ACM"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"C. Fischer. How to Combine Z with a Process Algebra. In J. Bowen, A. Fett, and M. Hinchey, editors, ZUM\u201998: The Z Formal Specification Notation. Springer-Verlag, 1998.","DOI":"10.1007\/978-3-540-49676-2_2"},{"key":"26_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/3-540-16442-1_14","volume-title":"ESOP\u201986 European Symposium on Programming","author":"J. He","year":"1986","unstructured":"J. He, C. A. R. Hoare, and J. W. Sanders. Data Refinement Refined. In G. Goos and H. Hartmants, editors, ESOP\u201986 European Symposium on Programming, volume 213 of Lecture Notes in Computer Science, pages 187\u2013196, March 1986."},{"key":"26_CR6","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:576\u2013580, 1969.","journal-title":"Communications of the ACM"},{"key":"26_CR7","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. Acta Informatica, 1:271\u2013281, 1972.","journal-title":"Acta Informatica"},{"key":"26_CR8","unstructured":"C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall International, 1985."},{"key":"26_CR9","doi-asserted-by":"crossref","unstructured":"C. A. R. Hoare and He Jifeng. Unifying Theories of Programming. Prentice-Hall, 1998.","DOI":"10.1007\/BFb0002714"},{"key":"26_CR10","unstructured":"C. C. Morgan. Programming from Specifications. Prentice-Hall, 2nd edition, 1994."},{"issue":"6","key":"26_CR11","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/BF00277386","volume":"27","author":"C. C. Morgan","year":"1990","unstructured":"C. C. Morgan and P. H. B. Gardiner. Data Refinement by Calculation. Acta Informatica, 27(6):481\u2013503, 1990.","journal-title":"Acta Informatica"},{"issue":"3","key":"26_CR12","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/0167-6423(87)90011-6","volume":"9","author":"J. M. Morris","year":"1987","unstructured":"J. M. Morris. A Theoretical Basis for Stepwise Refinement and the Programming Calculus. Science of Computer Programming, 9(3):287\u2013306, 1987.","journal-title":"Science of Computer Programming"},{"key":"26_CR13","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S. Owicki","year":"1976","unstructured":"S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Acta Informatica, 6:319\u2013340, 1976.","journal-title":"Acta Informatica"},{"issue":"5","key":"26_CR14","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/360051.360224","volume":"19","author":"S. Owicki","year":"1976","unstructured":"S. Owicki and D. Gries. Verifying properties of parallel programs: an axiomatic approach. Communications of the ACM, 19(5):279\u2013285, 1976.","journal-title":"Communications of the ACM"},{"key":"26_CR15","unstructured":"A. W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall Series in Computer Science. Prentice-Hall, 1998."},{"key":"26_CR16","unstructured":"J. M. Spivey. The Z Notation: A Reference Manual. Prentice-Hall, 2nd edition, 1992."},{"key":"26_CR17","series-title":"Technical report","volume-title":"Circus: a concurrent refinement language","author":"J. C. P. Woodcock","year":"2001","unstructured":"J. C. P. Woodcock and A. L. C. Cavalcanti. Circus: a concurrent refinement language. Technical report, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford OX1 3QD UK, July 2001."},{"key":"26_CR18","unstructured":"J. C. P. Woodcock and A. L. C. Cavalcanti. A concurrent language for refinement. In Andrew Butterfield and Claus Pahl, editors, IWFM\u201901: 5th Irish Workshop in Formal Methods. Computer Science Department, Trinity College Dublin, July 2001."},{"key":"26_CR19","unstructured":"J. C. P. Woodcock and A. L. C. Cavalcanti. The steam boiler in a unified theory of Z and CSP. In 8th Asia-Pacific Software Engineering Conference (APSEC 2001), 2001."},{"key":"26_CR20","doi-asserted-by":"crossref","unstructured":"J. C. P. Woodcock and A. L. C. Cavalcanti. The Semantics of Circus. In ZB 2002 International Conference, 2002. To appear.","DOI":"10.1007\/3-540-45648-1_10"},{"key":"26_CR21","unstructured":"J. C. P. Woodcock and J. Davies. Using Z-Specification, Refinement, and Proof. Prentice-Hall, 1996."}],"container-title":["Lecture Notes in Computer Science","FME 2002:Formal Methods\u2014Getting IT Right"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45614-7_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T11:09:21Z","timestamp":1737025761000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45614-7_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439288","9783540456148"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-45614-7_26","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"9 July 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}