{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:04:33Z","timestamp":1770282273424,"version":"3.49.0"},"reference-count":23,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[1990,3,1]],"date-time":"1990-03-01T00:00:00Z","timestamp":636249600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1990,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>A theory of commands with weakest precondition semantics is formalised using the HOL proof assistant system. The concept of refinement between commands is formalised, a number of refinement rules are proved and it is shown how the formalisation can be used for proving refinements of actual program texts correct.<\/jats:p>","DOI":"10.1007\/bf01888227","type":"journal-article","created":{"date-parts":[[2005,7,4]],"date-time":"2005-07-04T21:23:27Z","timestamp":1120512207000},"page":"247-272","source":"Crossref","is-referenced-by-count":48,"title":["Refinement concepts formalised in higher order logic"],"prefix":"10.1145","volume":"2","author":[{"given":"R. J. R.","family":"Back","sequence":"first","affiliation":[{"name":"Department of Computer Science, \u00c5bo Akademi University, Lemmink\u00e4isenkatu 14, SF-20520, Turku, Finland"}]},{"given":"J.","family":"von Wright","sequence":"additional","affiliation":[{"name":"Swedish School of Economics and Business Education, Biblioteksgatan 16, SF-65100 Vasa, Finland"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Back R. J. R.: On the Correctness of Refinement in Program Development Ph.D. thesis Report A-1978-4 Department of Computer Science University of Helsinki 1978."},{"key":"e_1_2_1_2_2_2","unstructured":"Back R. J. R.: Correctness Preserving Program Refinements: Proof Theory and Applications Vol. 131 of Mathematical Centre Tracts Mathematical Centre Amsterdam 1980."},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00291051"},{"key":"e_1_2_1_2_4_2","volume-title":"Refining Atomicity in Parallel Algorithms","author":"Back R. J. R.","year":"1989"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Back R. J. R. and Sere K.: Stepwise Refinement of Action Systems. In: Mathematics of Program Construction Lecture Notes in Computer Science 375 Springer-Verlag 1989.","DOI":"10.1007\/3-540-51305-1_7"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Back R. J. R. and Wright J. von: A Lattice-Theoretical Basis for a Specification Language. In: Mathematics of Program Construction Lecture Notes in Computer Science 375 Springer-Verlag 1989.","DOI":"10.1007\/3-540-51305-1_8"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Back R. J. R. and Wright J. von: Refinement Calculus part I: Sequential Programs. In: REX Workshop for Refinement of Distributed Systems Nijmegen The Netherlands 1989.","DOI":"10.1007\/3-540-52559-9_60"},{"key":"e_1_2_1_2_8_2","unstructured":"Gardiner P. H. Morgan C. C. and Robinson K. A.: On the Refinement Calculus. Techn. Rep. PRG 70 Programming Research Group Oxford University 1988."},{"key":"e_1_2_1_2_9_2","unstructured":"Dijkstra E. W.: A Discipline of Programming Prentice-Hall International 1976."},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268074"},{"key":"e_1_2_1_2_11_2","unstructured":"Gardiner P. H. and Morgan C. C. Data refinement of predicate transformers. Theoretical Computer Science . (To appear.)"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Gordon M. J. C.: HOL: A Proof Generating System for Higher-Order Logic. In: VLSI 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":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Gordon M. J. C.: Mechanizing Programming Logics in Higher-Order Logic. In: Current 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"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Gries D.: The Science of Programming Springer-Verlag 1981.","DOI":"10.1007\/978-1-4612-5983-1"},{"key":"e_1_2_1_2_15_2","unstructured":"Mason I. A.: Hoare's Logic in the LF. Techn. Rep. 87-32 Laboratory for Foundations of Computer Science University of Edinburgh 1987."},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Melham T.: Automating Recursive Type Definitions in Higher Order Logic. In: Current 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_9"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Milner R. Gordon M. J. C. and Wadsworth C.: Edinburgh LCF: A mechanised logic of computation. Lecture Notes in Computer Science 78 Springer-Verlag 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"e_1_2_1_2_18_2","unstructured":"Morgan C. C.: Programming from Specifications Prentice-Hall 1990."},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90011-6"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Park D.: On the semantics of fair parallelism. In: Lecture Notes in Computer Science 86 pp. 504\u2013526 Springer-Verlag 1980.","DOI":"10.1007\/3-540-10007-5_47"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/9758.11326"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_2_1_2_23_2","unstructured":"Wright J. von: Stepwise Derivation of a Parallel Matrix Multiplication Algorithm. Reports on Computer Science and Mathematics 84 \u00c5bo Akademi 1989."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01888227.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01888227\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01888227","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:21:22Z","timestamp":1641482482000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01888227"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990,3]]},"references-count":23,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1990,3]]}},"alternative-id":["10.1007\/BF01888227"],"URL":"https:\/\/doi.org\/10.1007\/bf01888227","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1990,3]]}}}