{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T19:10:11Z","timestamp":1736536211072,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649878"},{"type":"electronic","value":"9783540498018"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055150","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T09:09:13Z","timestamp":1153991353000},"page":"423-441","source":"Crossref","is-referenced-by-count":0,"title":["A tool for data refinement"],"prefix":"10.1007","author":[{"given":"Rimvydas","family":"Ruk\u0161\u0117nas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joakim","family":"von Wright","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"key":"25_CR1","volume-title":"volume 131 of Mathematical Center Tracts","author":"R. J. Back","year":"1980","unstructured":"R. J. Back. Correctness Preserving Program Refinements: Proof Theory and Applications, volume 131 of Mathematical Center Tracts. Mathematical Centre, Amsterdam, 1980."},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"R. J. Back and R. Kurki-Suonio. Decentralisation of process nets with centralised control. In 2nd ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing, pages 131\u2013142, 1983.","DOI":"10.1145\/800221.806716"},{"key":"25_CR3","first-page":"17","volume":"12","author":"R. J. Back","year":"1991","unstructured":"R. J. Back and K. Sere. Stepwise refinement of action systems. Structured Programming, 12:17\u201330, Sept. 1991.","journal-title":"Structured Programming"},{"key":"25_CR4","unstructured":"R. J. Back and J. von Wright. Reasoning algebraically about loops. Technical Report 144, Turku Centre for Computer Science, November 1997."},{"key":"25_CR5","unstructured":"M. J. 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'97, Discrete Mathematics and Theoretical Computer Science, 1997. Springer-Verlag."},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"D. Carrington, I. Hayes, R. Nickson, G. Watson, and J. Welsh. A tool for developing correct programs by refinement. In H. Jifeng, editor, BGS FACS 7th Refinement Workshop. Springer-Verlag, July 1996.","DOI":"10.14236\/ewic\/RW1996.3"},{"key":"25_CR7","unstructured":"E. W. Dijkstra. A Discipline of Programming. Prentice-Hall Series in Automatic Computation. Prentice Hall, 1976."},{"key":"25_CR8","unstructured":"M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"25_CR9","first-page":"272","volume-title":"A tactic driven refinement tool","author":"L. J. Groves","year":"1992","unstructured":"L. J. Groves, R. G. Nickson, and M. Utting. A tactic driven refinement tool. In C. B. Jones, B. T. Denvir, and R. C. F. Shaw, editors, 5th Refinement Workshop, Workshops in Computing, pages 272\u2013297, London, Jan. 1992. BCS-FACS, Springer-Verlag."},{"key":"25_CR10","volume-title":"The HOL System","author":"J. Grundy","year":"1991","unstructured":"J. Grundy. The HOL window library. In The HOL System, volume Libraries. SRI International, Cambridge, England, 2.01 edition, July 1991.","edition":"2.01 edition"},{"issue":"4","key":"25_CR11","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(4):271\u2013281, 1972.","journal-title":"Acta Informatica"},{"issue":"8","key":"25_CR12","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1007\/BF01191809","volume":"30","author":"C. A. R. Hoare","year":"1993","unstructured":"C. A. R. Hoare, He Jifeng, and A. Sampaio. Normal Form Approach to Compiler Design. Acta Informatica, 30(8):701\u2013739, 1993.","journal-title":"Acta Informatica"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"H.-M. J\u00c4rvinen and R. Kurki-Suonio. DisCo specification language: marriage of actions and objects. in Proc. of 11th Int. Conf. on Distributed Computing Systems, pages 142\u2013151, IEEE Computer Society, 1991.","DOI":"10.1109\/ICDCS.1991.148656"},{"key":"25_CR14","unstructured":"C. B. Jones. Systematic Software Development using VDM. Prentice-Hall, 1986."},{"key":"25_CR15","unstructured":"L. Laibinis and J. von Wright. Context handling in the refinement calculus framework. Technical Report 118, Turku Centre for Computer Science, June 1997."},{"key":"25_CR16","unstructured":"P. Lucas. Two constructive realizations of the block concept and their equivalence. Technical Report TR 25.085, IBM Laboratory Vienna, 1968."},{"key":"25_CR17","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/0020-0190(88)90227-X","volume":"29","author":"C. C. Morgan","year":"1988","unstructured":"C. C. Morgan. Auxiliary variables in data refinement. Information Processing Letters, 29:293\u2013296, 1988.","journal-title":"Information Processing Letters"},{"key":"25_CR18","unstructured":"C. C. Morgan. Programming from Specifications. Prentice Hall, 2nd edition, 1994."},{"issue":"6","key":"25_CR19","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. Gardiner. Data refinement by calculation. Acta Informatica, 27(6):481\u2013503, 1990.","journal-title":"Acta Informatica"},{"issue":"4","key":"25_CR20","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00276019","volume":"26","author":"J. M. Morris","year":"1989","unstructured":"J. M. Morris. Laws of data refinement. Acta Informatica, 26(4):287\u2013308, 1989.","journal-title":"Acta Informatica"},{"key":"25_CR21","unstructured":"J. K. Ousterhout. Tcl and the Tk Toolkit. Addison Wesley, 1994."},{"key":"25_CR22","doi-asserted-by":"crossref","unstructured":"J. Shield, R. Nickson and D. Carrington. Supporting Data Refinement in a Program Refinement Tool. In L. Groves and S. Reeves, editors, Formal Methods Pacific'97, Discrete Mathematics and Theoretical Computer Science, 1997. Springer-Verlag.","DOI":"10.1007\/s001650050006"},{"key":"25_CR23","first-page":"121","volume-title":"Workshops in Computing","author":"J. Wright von","year":"1994","unstructured":"J. von Wright. Program refinement by theorem prover. In D. Till and R.C.F. Shaw, editors, 6th Refinement Workshop, Workshops in Computing, pages 121\u2013150, London, Jan. 1994. BCS-FACS, Springer-Verlag."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055150","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T03:15:03Z","timestamp":1736478903000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055150"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/bfb0055150","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}