{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:04:58Z","timestamp":1725573898959},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540204619"},{"type":"electronic","value":"9783540398936"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39893-6_23","type":"book-chapter","created":{"date-parts":[[2011,1,7]],"date-time":"2011-01-07T15:35:57Z","timestamp":1294414557000},"page":"396-415","source":"Crossref","is-referenced-by-count":1,"title":["A Refinement Tool for Z"],"prefix":"10.1007","author":[{"given":"Angela","family":"Freitas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carla","family":"Nascimento","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"23_CR1","unstructured":"ISO\/IEC 13568: Information technology\u2014Z formal specification notation\u2014 syntax, type system and semantics. International Standard (2002)"},{"key":"23_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Progams to Meanings","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book: Assigning Progams to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"23_CR3","unstructured":"Back, R.J.R.: Procedural Abstraction in the Refinement Calculus. Technical report, Department of Computer Science, \u00c5bo, Finland, Ser. A No. 55 (1987)"},{"key":"23_CR4","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/BF01888227","volume":"2","author":"R.J.R. Back","year":"1990","unstructured":"Back, R.J.R., Wright, J.: Refinement Concepts Formalised in Higher Order Logic. Formal Aspects of Computing\u00a02, 247\u2013274 (1990)","journal-title":"Formal Aspects of Computing"},{"key":"23_CR5","volume-title":"FMP 1997 \u2013 Formal Methods Pacific","author":"M.J. Butler","year":"1997","unstructured":"Butler, M.J., Grundy, J., Langbacka, T., Rukvenas, R., Wright, J.: The Refinement Calculator \u2013 Proof Support for Program Refinement. In: FMP 1997 \u2013 Formal Methods Pacific. Springer, Heidelberg (1997)"},{"issue":"2","key":"23_CR6","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s001650050006","volume":"10","author":"D. Carrington","year":"1998","unstructured":"Carrington, D., Hayes, I., Nickson, R., Watson, G., Welsh, J.: A program Refinement Tool. Formal Aspects of Computing\u00a010(2), 97\u2013124 (1998)","journal-title":"Formal Aspects of Computing"},{"key":"23_CR7","unstructured":"Cavalcanti, A.L.C.: A Refinement Calculus for Z. PhD thesis, Oxford University Computing Laboratory, Oxford - UK, Technical Monograph TM-PRG-123 (1997) ISBN 00902928-97-X"},{"issue":"1","key":"23_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1590\/S0104-65001998000200002","volume":"5","author":"A.L.C. Cavalcanti","year":"1998","unstructured":"Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: Procedures and Recursion in the Refinement Calculus. Journal of the Brazilian Computer Society\u00a05(1), 1\u201315 (1998)","journal-title":"Journal of the Brazilian Computer Society"},{"issue":"1","key":"23_CR9","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/S0167-6423(97)00015-4","volume":"33","author":"A.L.C. Cavalcanti","year":"1999","unstructured":"Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: An Inconsistency in Procedures, Parameters, and Substitution the Refinement Calculus. Science of Computer Programming\u00a033(1), 87\u201396 (1999)","journal-title":"Science of Computer Programming"},{"issue":"1","key":"23_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1093\/comjnl\/41.1.1","volume":"41","author":"A.L.C. Cavalcanti","year":"1998","unstructured":"Cavalcanti, A.L.C., Woodcock, J.C.P.: A Weakest Precondition Semantics for Z. The Computer Journal\u00a041(1), 1\u201315 (1998)","journal-title":"The Computer Journal"},{"issue":"3","key":"23_CR11","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/s001650050016","volume":"10","author":"A.L.C. Cavalcanti","year":"1999","unstructured":"Cavalcanti, A.L.C., Woodcock, J.C.P.: ZRC\u2014A Refinement Calculus for Z. Formal Aspects of Computing\u00a010(3), 267\u2013289 (1999)","journal-title":"Formal Aspects of Computing"},{"key":"23_CR12","unstructured":"Coutinho, S.L., Reis, T.P.C., Cavalcanti, A.L.C.: Uma Ferramenta Educacional de Refinamentos. In: XIII Simp\u00f3sio Brasileiro de Engenharia de Software, Florian\u00f3polis - SC, pp. 61\u201364. Sess\u00e3o de Ferramentas (1999)"},{"key":"23_CR13","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","year":"1993","key":"23_CR14","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"23_CR15","unstructured":"Groves, L.: Adapting Formal Derivations. Technical Report CS-TR-95-9, Victoria University of Wellington (1995)"},{"key":"23_CR16","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1007\/978-1-4471-3550-0_14","volume-title":"5th Refinement Workshop, Workshops in Computing","author":"L. Groves","year":"1992","unstructured":"Groves, L., Nickson, R., Utting, M.: A Tactic Driven Refinement Tool. In: Jones, C.B., Shaw, R.C., Denvir, T. (eds.) 5th Refinement Workshop, Workshops in Computing, pp. 272\u2013297. Springer, Heidelberg (1992)"},{"key":"23_CR17","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1007\/978-1-4471-3550-0_12","volume-title":"5th Refinement Workshop, Workshops in Computing","author":"J. Grundy","year":"1992","unstructured":"Grundy, J.: A Window Inference Tool for Refinement. In: Jones, C.B., Shaw, R.C., Denvir, T. (eds.) 5th Refinement Workshop, Workshops in Computing, pp. 230\u2013254. Springer, Heidelberg (1992)"},{"key":"23_CR18","series-title":"ch. 11","first-page":"253","volume-title":"Applications of Formal Methods","author":"U. Hamer","year":"1995","unstructured":"Hamer, U., Peleska, J.: Z Applied to the A330\/340 CIDS Cabin Communication System. In: Hinchey, M.G., Bowen, J.P. (eds.) Applications of Formal Methods. ch. 11, pp. 253\u2013284. Prentice-Hall, Englewood Cliffs (1995)"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1007\/3-540-52513-0_10","volume-title":"VDM \u201990. VDM and Z - Formal Methods in Software Development","author":"S. King","year":"1990","unstructured":"King, S.: Z and the Refinement Calculus. In: Langmaack, H., Hoare, C.A.R., Bjorner, D. (eds.) VDM 1990. LNCS, vol.\u00a0428, pp. 164\u2013188. Springer, Heidelberg (1990)"},{"key":"23_CR20","unstructured":"Laibinis, L.: Mechanised Formal Reasoning about Modular Programs. PhD thesis, Turku Centre for Computer Science (2000)"},{"key":"23_CR21","volume-title":"Programming from Specifications","author":"C.C. Morgan","year":"1994","unstructured":"Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice-Hall, Englewood Cliffs (1994)","edition":"2"},{"key":"23_CR22","doi-asserted-by":"crossref","unstructured":"Oliveira, M., Cavalcanti, A.L.C.: Tactics of Refinement. In: 14th Brazilian Symposium on Software Engineering, pp. 117\u2013132 (2000)","DOI":"10.5753\/sbes.2000.25924"},{"key":"23_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/3-540-57840-4_23","volume-title":"Programming Languages and System Architectures","author":"J.L.A. Snepscheut","year":"1994","unstructured":"Snepscheut, J.L.A.: Mechanised Support for Stepwise Refinement. In: Gutknecht, J. (ed.) Programming Languages and System Architectures. LNCS, vol.\u00a0782, pp. 35\u201348. Springer, Heidelberg (1994)"},{"key":"23_CR24","volume-title":"The Z Notation: A Reference Manual","author":"J.M. Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice-Hall, Englewood Cliffs (1992)","edition":"2"},{"key":"23_CR25","unstructured":"Staples, M.: A Mechanised Theory of Refinement. PhD thesis, Cambridge University (1999)"},{"key":"23_CR26","unstructured":"Utting, M.: The ergo5 generic proof engine. Technical Report 97-44, Software Verification Research Centre (1997)"},{"key":"23_CR27","unstructured":"Vickers, T.: An Overview of a Refinement Editor. In: 5th Australian Software Engineering Conference, Sidney, Australia, pp. 39\u201344 (1990)"},{"key":"23_CR28","volume-title":"5th Refinement Workshop,Workshops in Computing","author":"J.C.P. Woodcock","year":"1992","unstructured":"Woodcock, J.C.P.: Implementing Promoted Operations in Z. In: Jones, C.B., Shaw, R.C., Denvir, T. (eds.) 5th Refinement Workshop,Workshops in Computing, London - UK. Prentice-Hall, Englewood Cliffs (1992)"},{"key":"23_CR29","volume-title":"Using Z\u2014Specification, Refinement, and Proof","author":"J.C.P. Woodcock","year":"1996","unstructured":"Woodcock, J.C.P., Davies, J.: Using Z\u2014Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)"},{"key":"23_CR30","first-page":"121","volume-title":"6th Refinement Workshop, Workshops in Computing","author":"J. Wright","year":"1994","unstructured":"Wright, J.: Program Refinement by Theorem Prover. In: Till, D. (ed.) 6th Refinement Workshop, Workshops in Computing, London - UK, pp. 121\u2013150. Springer, Heidelberg (1994)"},{"key":"23_CR31","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/BF01383984","volume":"3","author":"J. Wright","year":"1993","unstructured":"Wright, J., Hekanaho, J., Luostarinen, P., Langbacka, T.: Mechanizing Some Advanced Refinement Concepts. Formal Methods in System Design\u00a03, 49\u201381 (1993)","journal-title":"Formal Methods in System Design"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39893-6_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,2]],"date-time":"2024-04-02T21:00:57Z","timestamp":1712091657000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39893-6_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540204619","9783540398936"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39893-6_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}