{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,28]],"date-time":"2026-06-28T04:57:35Z","timestamp":1782622655718,"version":"3.54.5"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[1993,8,1]],"date-time":"1993-08-01T00:00:00Z","timestamp":744163200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1993,8]]},"DOI":"10.1007\/bf01383984","type":"journal-article","created":{"date-parts":[[2005,4,2]],"date-time":"2005-04-02T02:08:55Z","timestamp":1112407735000},"page":"49-81","source":"Crossref","is-referenced-by-count":17,"title":["Mechanizing some advanced refinement concepts"],"prefix":"10.1007","volume":"3","author":[{"given":"J.","family":"Von Wright","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"J.","family":"Hekanaho","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"P.","family":"Luostarinen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"T.","family":"L\u00e5ngbacka","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"593","DOI":"10.1007\/BF00291051","volume":"25","author":"R.J.R. Back","year":"1988","unstructured":"R.J.R. Back. A calculus of refinements for program derivations.Acta Informatica, 25:593?624, 1988.","journal-title":"Acta Informatica"},{"key":"CR2","unstructured":"C.C. Morgan.Programming from Specifications. Prentice-Hall, 1990."},{"key":"CR3","unstructured":"E.W. Dijkstra.A Discipline of Programming. Prentice-Hall International, 1976."},{"key":"CR4","doi-asserted-by":"crossref","unstructured":"R.J.R. Back. Changing data representation in the refinement calculus. In21st Hawaii International Conference on System Sciences, January, 1989.","DOI":"10.1109\/HICSS.1989.47997"},{"issue":"1","key":"CR5","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1016\/0304-3975(91)90029-2","volume":"87","author":"P.H. Gardiner","year":"1991","unstructured":"P.H. Gardiner and C.C. Morgan. Data refinement of predicate transformers.Theoretical Cumputer Science, 87(1):143?162, 1991.","journal-title":"Theoretical Cumputer Science"},{"key":"CR6","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:287?308, 1989.","journal-title":"Acta Informatica"},{"key":"CR7","unstructured":"C.B. Jones.Systematic Software Development Using VDM. Prentice-Hall International, 1986."},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"K.M. Chandy and J. Misra.Parallel Program Design: A Foundation. Addison-Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"L. Boug\u00e9 and N. Francez. A compositional approach to superposition. InProc. 14th Conference on Principles of Programming Languages, San Diego, USA, January 1988, 240?249.","DOI":"10.1145\/73560.73581"},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"R.J.R. Back and K. Sere. Superposition refinement of parallel algorithms. InFormal Description Techniques IV, K.R. Parker and G.A. Rose, (eds.), Elsevier Science Publishers (North-Holland) 1992, 475?493.","DOI":"10.1016\/B978-0-444-89402-1.50044-8"},{"key":"CR11","unstructured":"D.M. Goldschlag. Mechanizing UNITY. InTC2 Working Conference on Programming Concepts and Methods, M. Broy, (ed.), Israel, 1990, IFIP, 374?401."},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"U. Engberg, P. Groenning and L. Lamport. Mechanical verification of concurrent systems with TLA. InProc. 4th Workshop on Computer-Aided Verification, Montreal, Canada. June, 1992, Springer-Verlag.","DOI":"10.1007\/3-540-56496-9_5"},{"key":"CR13","unstructured":"M. Aagard and M. Leeser. Verifying a logic synthesis tool in Nuprl. InProc. 4th Workshop on Computer-Aided Verification, Montreal, Canada, June, 1992, Springer-Verlag."},{"key":"CR14","doi-asserted-by":"crossref","unstructured":"M.J.C. Gordon. HOL: A proof generating system for higher-order logic. InVLSI Specification, Verification and Synthesis, G. Birtwistle and P.A. Subrahmanyam (eds.), Kluwer Academic Publishers, 1988.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"M.J.C. Gordon. Mechanizing programming logics in higher-order logic. InCurrent Trends in Hardware Verification and Theorem Proving, G. Birtwistle and P.A. Subrahmanyam (eds.), Springer-Verlag, 1989.","DOI":"10.1007\/978-1-4612-3658-0_10"},{"issue":"9","key":"CR16","doi-asserted-by":"crossref","first-page":"993","DOI":"10.1109\/32.58786","volume":"16","author":"A.J. Camilleri","year":"1990","unstructured":"A.J. Camilleri. Mechanizing CSP trace theory in higher order logic.IEEE Transactions of Software Engineering, 16(9):993?1004, 1990.","journal-title":"IEEE Transactions of Software Engineering"},{"key":"CR17","volume-title":"A Theorem Prover for UNITY in Higher Order Logic","author":"F. Andersen","year":"1992","unstructured":"F. Andersen. A Theorem Prover for UNITY in Higher Order Logic. PhD thesis, Technical University of Denmark, Lyngby Denmark, 1992."},{"key":"CR18","unstructured":"S. Agerholm. Mechanizing program verification in HOL. DAIMI IR-111, Aarhus University, 1992."},{"key":"CR19","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/BF01888227","volume":"2","author":"R.J.R. Back","year":"1990","unstructured":"R.J.R. Back and J. von Wright. Refinement concepts formalised in higher-order logic.Formal Aspects of Computing, 2:247?272, 1990.","journal-title":"Formal Aspects of Computing"},{"key":"CR20","doi-asserted-by":"crossref","unstructured":"J. Grundy. A window inference tool for refinement. InProc. 5th Refinement Workshop, Jones et al. (ed.), London, Jan. 1992, Springer-Verlag.","DOI":"10.1007\/978-1-4471-3550-0_12"},{"key":"CR21","unstructured":"T. Vickers. An overview of a refinement editor. In5th Australian Software Engineering Conference, Sydney, May 1990."},{"key":"CR22","doi-asserted-by":"crossref","unstructured":"L. Groves and R. Nickson. A tactic driven refinement tool. InProc. 5th Refinement Workshop, Jones et al. (ededs.), London, Jan., 1992, Springer-Verlag.","DOI":"10.1007\/978-1-4471-3550-0_14"},{"key":"CR23","doi-asserted-by":"crossref","unstructured":"J. von Wright and K. Sere. Program transformations and refinements in HOL. InProc. 1991 International Workshop on Higher Order Logic Theorem Proving and its Applications, Davis, USA, August, 1991. IEEE\/ACM.","DOI":"10.1109\/HOL.1991.596290"},{"key":"CR24","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"A. Church. A formulation of the simple theory of types.Journal of Symbolic Logic, 5:56?68, 1940.","journal-title":"Journal of Symbolic Logic"},{"key":"CR25","doi-asserted-by":"crossref","unstructured":"E.W. Dijkstra and C.S. Scholten.Predicate Calculus and Program Semantics. Springer-Verlag, 1990.","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"CR26","series-title":"volume 131 of Mathematical Center Tracts","volume-title":"Correctness Preserving Program Refinements: Proof Theory and Applications","author":"R.J.R. Back","year":"1980","unstructured":"R.J.R. Back.Correctness Preserving Program Refinements: Proof Theory and Applications, volume 131 of Mathematical Center Tracts. Mathematical Centre, Amsterdam, 1980."},{"key":"CR27","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1016\/0020-0190(88)90147-0","volume":"26","author":"C.C. Morgan","year":"1988","unstructured":"C.C. Morgan. Data refinement by miracles.Information Processing Letters, 26:243?246, January, 1988.","journal-title":"Information Processing Letters"},{"key":"CR28","doi-asserted-by":"crossref","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:287?306, 1987.","journal-title":"Science of Computer Programming"},{"key":"CR29","first-page":"17","volume":"12","author":"R.J.R. Back","year":"1991","unstructured":"R.J.R. Back and K. Sere. Stepwise refinement of action systems.Structured Programming, 12:17?30 1991.","journal-title":"Structured Programming"},{"key":"CR30","series-title":"volume 430 of Lecture Notes in Computer Science","volume-title":"REX Workshop for Refinement of Distributed Systems","author":"R.J.R. Back","year":"1989","unstructured":"R.J.R. Back. Refinement Calculus, part II: Parallel and reactive programs. InREX Workshop for Refinement of Distributed Systems, volume 430 of Lecture Notes in Computer Science, Nijmegen, The Netherlands, 1989, Springer-Verlag."},{"key":"CR31","series-title":"volume 430 of Lecture Notes in Computer Science","volume-title":"REX Workshop for Refinement of Distributed Systems","author":"R.J.R. Back","year":"1989","unstructured":"R.J.R. Back and J. von Wright. Refinement calculus, part 1: Sequential programs. InREX Workshop for Refinement of Distributed Systems, volume 430 of Lecture Notes in Computer Science, Nijmegen, the Netherlands, 1989, Springer-Verlag."},{"key":"CR32","unstructured":"J. von Wright. The lattice of data refinement. Reports on computer science and mathematics 130, \u00c5bo Akademi, 1992. To appear inActa Informatica"},{"key":"CR33","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1016\/0304-3975(92)90309-4","volume":"100","author":"R.J.R. Back","year":"1992","unstructured":"R.J.R., Back and J. von Wright. Combining angels, demons and miracles in program specifications.Theoretical Computer Science, 100:365?383, 1992.","journal-title":"Theoretical Computer Science"},{"key":"CR34","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/0020-0190(87)90224-9","volume":"25","author":"J. He","year":"1987","unstructured":"J. He, C.A.R. Hoare and J.W. Sanders. Prespecification in data refinement.Information Processing Letters, 25:71?76, 1987.","journal-title":"Information Processing Letters"},{"key":"CR35","series-title":"volume 430 of Lecture Notes in Computer Science","volume-title":"REX Workshop for Refinement of Distributed Systems","author":"B. Jonsson","year":"1989","unstructured":"B. Jonsson. On decomposing and refining specifications of distributed systems. InREX Workshop for Refinement of Distributed Systems, volume 430 of Lecture Notes in Computer Science, Nijmegen, The Netherlands, 1989, Springer-Verlag."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01383984.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01383984\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01383984","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,24]],"date-time":"2024-01-24T13:23:07Z","timestamp":1706102587000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01383984"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,8]]},"references-count":35,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1993,8]]}},"alternative-id":["BF01383984"],"URL":"https:\/\/doi.org\/10.1007\/bf01383984","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,8]]}}}