{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:14:20Z","timestamp":1763468060523},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540601173"},{"type":"electronic","value":"9783540494454"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60117-1_8","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:44:05Z","timestamp":1330278245000},"page":"128-158","source":"Crossref","is-referenced-by-count":10,"title":["Exploring summation and product operators in the refinement calculus"],"prefix":"10.1007","author":[{"given":"Ralph-Johan","family":"Back","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Butler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"8_CR1","unstructured":"J.R. Abrial. The B-Book. To be published by Cambridge University Press, 1995."},{"key":"8_CR2","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. Tract 131, Mathematisch Centrum, Amsterdam, 1980."},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"R.J.R. 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":"8_CR4","doi-asserted-by":"crossref","unstructured":"R.J.R. Back and K. Sere. Superposition refinement of parallel algorithms. In K.A. Parker and G.A. Rose, editors, FORTE'91. North-Holland, 1992.","DOI":"10.1016\/B978-0-444-89402-1.50044-8"},{"key":"8_CR5","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/BF01888227","volume":"5","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, 5:247\u2013272, 1990.","journal-title":"Formal Aspects of Computing"},{"key":"8_CR6","unstructured":"R.J.R. Back and J. von Wright. Refinement Calculus. Book in preparation, \u00c5bo Akademi, 1994."},{"key":"8_CR7","unstructured":"M.J. Butler. A CSP Approach To Action Systems. D.Phil. Thesis, Programming Research Group, Oxford University, 1992."},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"M.J. Butler. Refinement and Decomposition of Value-Passing Action Systems. In E. Best, editor, CONCUR'93, volume LNCS 715. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-57208-2_16"},{"key":"8_CR9","unstructured":"E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976."},{"key":"8_CR10","unstructured":"E.W. Dijkstra. From Predicate Transformers to Predicates. Manuscript EWD821, April 1982."},{"key":"8_CR11","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1016\/0304-3975(91)90029-2","volume":"87","author":"P.H.B. Gardiner","year":"1991","unstructured":"P.H.B. Gardiner and C.C. Morgan. Data refinement of predicate transformers. Theoretical Computer Science, 87:143\u2013162, 1991.","journal-title":"Theoretical Computer Science"},{"key":"8_CR12","volume-title":"Lecture Notes from Eastern Finland Universities International Summer School on Novel Computing","author":"J. Gutknecht","year":"1994","unstructured":"J. Gutknecht. Object-Oriented Programming with Oberon. Lecture Notes from Eastern Finland Universities International Summer School on Novel Computing, Lapeenranta University of Technology, Finland, 1994."},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"J. He, C.A.R. Hoare, and J.W. Sanders. Data refinement refined. In European Symposium on Programming, volume LNCS 213. Springer-Verlag, 1986.","DOI":"10.1007\/3-540-16442-1_14"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"issue":"1\u20132","key":"8_CR15","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0167-6423(94)90008-6","volume":"22","author":"P.F. Hoogendijk","year":"1994","unstructured":"P.F. Hoogendijk and R.C. Backhouse. Relational programming laws in the tree, list, bag, set hierarchy. Science of Computer Programming, 22(1\u20132):67\u2013105, 1994.","journal-title":"Science of Computer Programming"},{"key":"8_CR16","unstructured":"He Jifeng and C.A.R. Hoare. Categorical Semantics of Programming Languages. In Mathematical Foundations of Programming Semantics, volume LNCS 442. Springer-Verlag, 1990."},{"key":"8_CR17","unstructured":"C.B. Jones. Systematic Software Development using VDM \u2014 Second Edition. Prentice-Hall, 1990."},{"key":"8_CR18","unstructured":"C.E. Martin. Preordered Categories and Predicate Transformers. D.Phil. Thesis, Programming Research Group, Oxford University, 1991."},{"key":"8_CR19","unstructured":"C.C. Morgan. Programming from Specifications. Prentice-Hall, 1990."},{"key":"8_CR20","unstructured":"C.C. Morgan. The cuppest capjunctive capping, and Galois. In A.W. Roscoe, editor, A Classical Mind: Essays in Honour of C.A.R. Hoare. Prentice-Hall, 1994."},{"issue":"3","key":"8_CR21","doi-asserted-by":"crossref","first-page":"298","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):298\u2013306, 1987.","journal-title":"Science of Computer Programming"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"H.P. Mossenboeck. Object-Oriented Programming in Oberon-2. Springer-Verlag, 1994.","DOI":"10.1007\/978-3-642-79898-6"},{"key":"8_CR23","volume-title":"Ph.D. Thesis","author":"D.A. Naumann","year":"1992","unstructured":"D.A. Naumann. Two-Categories and Program Structure: Data Types, Refinement Calculi, and Predicate Transformers. Ph.D. Thesis, University of Texas at Austin, 1992."},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"D.A. Naumann. On the Essence of Oberon. In J. Gutknecht, editor, Conference on Programming Languages and System Architectures, volume LNCS 782. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-57840-4_39"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"D.A. Naumann. Data Refinement, Call by Value, and Higher Order Programs. Accepted for publication in Formal Aspects of Computing, 1995.","DOI":"10.1007\/BF01210999"},{"key":"8_CR26","unstructured":"J.M. Spivey. The Z Notation \u2014 A Reference Manual. Prentice-Hall, 1989."},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"B.M. Utting and K. Robinson. Modular reasoning in an object-oriented refinement calculus. In Mathematics of Program Construction, 1992, volume LNCS 669. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56625-2_22"},{"issue":"2","key":"8_CR28","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/BF01192157","volume":"31","author":"J. Wright von","year":"1994","unstructured":"J. von Wright. The lattice of data refinement. Acta Informatica, 31(2):105\u2013135, 1994.","journal-title":"Acta Informatica"},{"key":"8_CR29","unstructured":"N. Ward. Adding specification constructs to the refinement calculus. In FME'93, volume LNCS 670. Springer-Verlag, 1993."}],"container-title":["Lecture Notes in Computer Science","Mathematics of Program Construction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60117-1_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T09:26:19Z","timestamp":1640942779000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60117-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540601173","9783540494454"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-60117-1_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}