{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T08:45:31Z","timestamp":1773996331413,"version":"3.50.1"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2002,12,1]],"date-time":"2002-12-01T00:00:00Z","timestamp":1038700800000},"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":[[2002,12]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>Parallel computers have not yet had the expected impact on mainstream computing. Parallelism adds a level of complexity to the programming task that makes it very error-prone. Moreover, a large variety of very different parallel architectures exists. Porting an implementation from one machine to another may require substantial changes. This paper addresses some of these problems by developing a formal basis for the design of parallel programs in the form of a refinement calculus. The calculus allows the stepwise formal derivation of an abstract, low-level implementation from a trusted, high-level specification. The calculus thus helps structuring and documenting the development process. Portability is increased, because the introduction of a machine-dependent feature can be located in the refinement tree. Development efforts above this point in the tree are independent of that feature and are thus reusable. Moreover, the discovery of new, possibly more efficient solutions is facilitated. Last but not least, programs are correct by construction, which obviates the need for difficult debugging. Our programming\/specification notation supports fair parallelism, shared-variable and message-passing concurrency, local variables and channels. The calculus rests on a compositional trace semantics that treats shared-variable and message-passing concurrency uniformly. The refinement relation combines a context-sensitive notion of trace inclusion and assumption-commitment reasoning to achieve compositionality. The calculus straddles both concurrency paradigms, that is, a shared-variable program can be refined into a distributed, message-passing program and vice versa.<\/jats:p>","DOI":"10.1007\/s001650200032","type":"journal-article","created":{"date-parts":[[2003,3,24]],"date-time":"2003-03-24T21:54:03Z","timestamp":1048542843000},"page":"123-197","source":"Crossref","is-referenced-by-count":17,"title":["A Refinement Calculus for Shared-Variable Parallel and Distributed Programming"],"prefix":"10.1145","volume":"14","author":[{"given":"J.","family":"Dingel","sequence":"first","affiliation":[{"name":"School of Computing, Queen's University, Kingston, Ontario, Canada, , , , , , CA"}]}],"member":"320","reference":[{"key":"p_1","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/BFb0022461","volume-title":"Semantics of Concurrent Computation, LNCS 70","author":"Abrahamson K.","year":"1979"},{"key":"p_2","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","article-title":"The existence of refinement mappings","volume":"82","author":"Abadi M.","year":"1991","journal-title":"Theoretical Computer Science"},{"key":"p_3","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1145\/151646.151649","article-title":"Composing specifications","volume":"15","author":"Abadi M.","year":"1993","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"p_4","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1016\/0167-6423(83)90004-7","article-title":"-R.: Proof rules and transformations dealing with fairness","volume":"3","author":"Apt K. R.","year":"1983","journal-title":"Science of Computer Programming"},{"key":"p_5","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-4376-0","volume-title":"-R.: Verification of Sequential and Concurrent Programs","author":"Apt K.","year":"1991"},{"key":"p_6","volume-title":"J. W. de Bakker, W.-P","author":"Andrews G. R.","year":"1985"},{"key":"p_7","first-page":"60","article-title":"A ProCoS project description - ESPRIT BRA 3104","volume":"39","author":"Bj\u00f8rner D.","year":"1989","journal-title":"EATCS Bulletin"},{"key":"p_8","first-page":"67","volume-title":"REX Workshop on Stepwise Refinement of Distributed Systems, LNCS 430","author":"Back R. J. R.","year":"1989"},{"key":"p_9","volume-title":"LNCS 183","author":"Bauer F. L.","year":"1985"},{"key":"p_10","series-title":"NATO ASI Series F","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/978-3-642-58049-9_4","volume-title":"Software for Parallel Computation","author":"Block U.","year":"1993"},{"issue":"3","key":"p_11","doi-asserted-by":"crossref","first-page":"560","DOI":"10.1145\/828.833","article-title":"A theory of communicating sequential processes","volume":"31","author":"Brookes S. D.","year":"1984","journal-title":"Journal of the ACM"},{"key":"p_12","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(86)90040-X","article-title":"A theory for nondeterminism, parallelism, communication, and concurrency","volume":"45","author":"Broy M.","year":"1986","journal-title":"Theoretical Computer Science"},{"key":"p_14","volume-title":"Proceedings 11th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press","author":"Brookes S. D.","year":"1996"},{"issue":"2","key":"p_15","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1006\/inco.1996.0056","article-title":"Full abstraction for a shared-variable parallel language","volume":"127","author":"Brookes S. D.","year":"1996","journal-title":"Information and Computation"},{"key":"p_16","volume-title":"13th Annual Conference on Mathematical Foundations of Progamming Semantics (MFPS'13)","author":"Brookes S. D.","year":"1997"},{"key":"p_17","volume-title":"Broy and St\u00f8len","year":"2001"},{"key":"p_18","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/3-540-60043-4_64","volume-title":"Fourth International Conference on Algebraic Methodology and Software Technology (AMAST'95)","author":"Collette P.","year":"1995"},{"key":"p_19","volume-title":"Parallel Program Design: A Foundation","author":"Chandy K. M.","year":"1988"},{"key":"p_21","volume-title":"Second International Conference in Concurrency Theory (CONCUR'91)","author":"de Boer F. S.","year":"1991"},{"key":"p_22","first-page":"175","volume-title":"O.-J","author":"Dahl O.-J.","year":"1972"},{"key":"p_23","volume-title":": A Discipline of Programming","author":"Dijkstra E. W.","year":"1976"},{"key":"p_24","first-page":"703","volume-title":"Seventh International Conference in Concurrency Theory (CONCUR'96)","author":"Dingel J.","year":"1999"},{"key":"p_25","first-page":"320","volume-title":"J.: Approximating UNITY. In Second International Conference on Coordination Models and Languages (COORDINATION'97)","author":"Dingel","year":"1997"},{"key":"p_26","first-page":"231","volume-title":"Seventh International Conference on Algebraic Methodology and Software Technology (AMAST'98)","author":"Dingel J.","year":"1999"},{"key":"p_28","volume-title":"Data Refinement: Model-Oriented Methods and their Comparison","author":"de Roever W.-P.","year":"1999"},{"issue":"2","key":"p_29","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/BF00289074","article-title":"A proof method for cyclic programs","volume":"9","author":"Francez N.","year":"1978","journal-title":"Acta Informatica"},{"key":"p_30","volume-title":"Texts and Monographs in Computer Science","author":"Francez N.","year":"1986"},{"key":"p_31","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8596-5","volume-title":": A Practical Theory of Programming. Texts and Monographs in Computer Science","author":"Hehner C. R.","year":"1993"},{"key":"p_32","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/BF00289507","article-title":"Proof of correctness of data representations","volume":"4","author":"Hoare C. A. R.","year":"1972","journal-title":"Acta Informatica"},{"key":"p_33","volume-title":"C","author":"Jones","year":"1981"},{"key":"p_34","volume-title":"C","author":"Jones","year":"1990","edition":"2"},{"issue":"2","key":"p_36","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1016\/0304-3975(87)90007-7","article-title":"A context dependent equivalence between processes","volume":"49","author":"Larsen K. G.","year":"1987","journal-title":"Theoretical Computer Science"},{"key":"p_37","series-title":"NATO ASI Series F","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/978-3-642-58049-9_8","volume-title":"Software for Parallel Computation","author":"Levesque J. M.","year":"1993"},{"key":"p_39","volume-title":"OCCAM Programming Manual","author":"Ltd","year":"1984"},{"key":"p_40","first-page":"157","volume-title":"Proceedings Logic Colloquium '73","author":"Milner R.","year":"1973"},{"key":"p_41","volume-title":"Communication and Concurrency","author":"Milner R.","year":"1989"},{"issue":"3","key":"p_42","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/0167-6423(87)90011-6","article-title":"A theoretical basis for stepwise refinement and the programming calculus","volume":"9","author":"Morris J. M.","year":"1987","journal-title":"Science of Computer Programming"},{"issue":"3","key":"p_43","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1145\/44501.44503","article-title":"The specification statement","volume":"10","author":"Morgan C.","year":"1989","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"p_44","volume-title":"Programming from Specifications","author":"Morgan C.","year":"1994"},{"key":"p_45","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BF00268134","article-title":"An axiomatic proof technique for parallel programs","volume":"6","author":"Owicki S. S.","year":"1976","journal-title":"Acta Informatica"},{"key":"p_46","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511526589","volume-title":"Nets, Terms and Formulas","author":"Olderog E.-R.","year":"1991"},{"key":"p_48","first-page":"90","volume-title":"M.-C. Gaudel and J.-P","author":"Olderog E.-R.","year":"1993"},{"key":"p_50","series-title":"NATO ASI Series F","doi-asserted-by":"crossref","first-page":"216","DOI":"10.1007\/978-3-642-58049-9_16","volume-title":"Software for Parallel Computation","author":"Pancake C.","year":"1993"},{"key":"p_51","first-page":"504","volume-title":"Abstract Software Specifications, LNCS 86","author":"Park D.","year":"1979"},{"key":"p_52","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/978-3-642-82453-1_5","volume-title":"Logics and Models of Concurrent Systems, NATO ASI F13","author":"Pnueli A.","year":"1985"},{"key":"p_53","volume-title":": The Craft of Programming","author":"Reynolds J. C.","year":"1981"},{"key":"p_54","first-page":"1","article-title":"Specification and refinement of networks of asynchronously communicating agents using the assumption\/commitment paradigm","volume":"3","author":"St\u00f8len K.","year":"1995","journal-title":"Formal Aspects of Computing"},{"key":"p_56","volume-title":"Formal Methods for Parallel Programming and Applications Workshop at IPPS\/SPDP'98","author":"Skillicorn D.","year":"1998"},{"issue":"1","key":"p_57","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1049\/sej.1989.0006","article-title":"An introduction to Z and formal specification","volume":"4","author":"Spivey J. M.","year":"1989","journal-title":"Software Engineering Journal"},{"key":"p_58","volume-title":": The Z Notation: A Reference Manual","author":"Spivey J. M.","year":"1992"},{"key":"p_59","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1016\/0304-3975(88)90033-3","article-title":"A generalization of Owicki-Gries\u2019 Hoare logic for a concurrent while language","volume":"89","author":"Stirling C.","year":"1988","journal-title":"Theoretical Computer Science"},{"key":"p_61","first-page":"339","volume-title":"Semantics: Foundations and Applications","author":"Udink R. T.","year":"1993"},{"key":"p_62","first-page":"339","volume-title":"Fourth International Conference on Concurrency Theory (CONCUR'93)","author":"Udink R. T.","year":"1993"},{"issue":"8","key":"p_63","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1145\/79173.79181","article-title":"A briding model for parallel computation","volume":"33","author":"Valiant L. G.","year":"1990","journal-title":"Communications of the ACM"},{"key":"p_64","volume-title":"Fourth BCS-FACS Refinement Workshop","author":"Xu Q.","year":"1991"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s001650200032.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s001650200032\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s001650200032","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:31:06Z","timestamp":1641483066000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s001650200032"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,12]]},"references-count":55,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,12]]}},"alternative-id":["10.1007\/s001650200032"],"URL":"https:\/\/doi.org\/10.1007\/s001650200032","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,12]]}}}