{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T00:49:02Z","timestamp":1782953342218,"version":"3.54.5"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2016,11,1]],"date-time":"2016-11-01T00:00:00Z","timestamp":1477958400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,11,1]],"date-time":"2016-11-01T00:00:00Z","timestamp":1477958400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"publisher","award":["DP130102901"],"award-info":[{"award-number":["DP130102901"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2016,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The rely-guarantee technique allows one to reason compositionally about concurrent programs. To handle interference the technique makes use of rely and guarantee conditions, both of which are binary relations on states. A rely condition is an assumption that the environment performs only atomic steps satisfying the rely relation and a guarantee is a commitment that every atomic step the program makes satisfies the guarantee relation. In order to investigate rely-guarantee reasoning more generally, in this paper we allow interference to be represented by a process rather than a relation and hence derive more general rely-guarantee laws. The paper makes use of a weak conjunction operator between processes, which generalises a guarantee relation to a guarantee process, and introduces a rely quotient operator, which generalises a rely relation to a process. The paper focuses on the algebraic properties of the general rely-guarantee theory. The Jones-style rely-guarantee theory can be interpreted as a model of the general algebraic theory and hence the general laws presented here hold for that theory.<\/jats:p>","DOI":"10.1007\/s00165-016-0384-0","type":"journal-article","created":{"date-parts":[[2016,7,29]],"date-time":"2016-07-29T09:08:38Z","timestamp":1469783318000},"page":"1057-1078","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":27,"title":["Generalised rely-guarantee concurrency: an algebraic foundation"],"prefix":"10.1145","volume":"28","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3649-392X","authenticated-orcid":false,"given":"Ian J.","family":"Hayes","sequence":"first","affiliation":[{"name":"School of Information Technology and Electrical Engineering, The University of Queensland, Brisbane, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Aarts CJ (1992) Galois connections presented calculationally. Technical report Department of Computing Science Eindhoven University of Technology. Afstudeer verslag (Graduating Dissertation)"},{"key":"e_1_2_1_2_2_2","unstructured":"Aarts C Backhouse R Boiten E Doombos H van Gasteren N van Geldrop R Hoogendijk P Voermans E van der Woude J (1995) Fixed-point calculus. Inform Process Lett 53:131\u2013136. ( Mathematics of Program Construction Group )"},{"key":"e_1_2_1_2_3_2","unstructured":"Aczel PHG (1983) On an inference rule for parallel composition. Private communication to Cliff Jones. http:\/\/homepages.cs.ncl.ac.uk\/cliff.jones\/publications\/MSs\/PHGA-traces.pdf"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90005-2"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Backhouse R Crole R Gibbons J (eds) (2002) Algebraic and coalgebraic methods in the mathematics of program construction. Springer Berlin","DOI":"10.1007\/3-540-47797-7"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Blikle A (1978) Specified programming. In: Blum EK Paul M Takasu S (eds) Mathematical studies of information processing volume 75 of Lecture Notes in Computer Science. Springer Berlin pp 228\u2013251","DOI":"10.1007\/3-540-09541-1_29"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/s002360050163"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exm030"},{"key":"e_1_2_1_2_10_2","volume-title":"Regular algebra and finite machines","author":"Conway JH","year":"1971"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"de Boer FS Hannemann U de Roever W-P (1999) Formal justification of the rely-guarantee paradigm for shared-variable concurrency: a semantic approach. In: Wing J Woodcock J Davies J (eds) FM99 formal methods volume 1709 of Lecture Notes in Computer Science. Springer Berlin pp 1245\u20131265","DOI":"10.1007\/3-540-48118-4_16"},{"key":"e_1_2_1_2_12_2","unstructured":"Dingel J (2000) Systematic parallel programming. PhD thesis Carnegie Mellon University. CMU-CS-99-172"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200032"},{"key":"e_1_2_1_2_14_2","unstructured":"de Roever W-P (2001) Concurrency verification: introduction to compositional and noncompositional methods. Cambridge University Press Cambridge"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Hoare CAR He J (1986) The weakest prespecification. Fundamenta Informaticae IX:51\u201384","DOI":"10.3233\/FI-1986-9104"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Hoare CAR Hayes IJ He J Morgan C Roscoe AW Sanders JW S\u00f8rensen IH Spivey JM Sufrin BA (1987) Laws of programming. Commun ACM 30(8):672\u2013686. Corrigenda: CACM 30(9):770","DOI":"10.1145\/27651.27653"},{"key":"e_1_2_1_2_17_2","unstructured":"Hayes IJ Jones CB Colvin RJ (2014) Laws and semantics for rely-guarantee refinement. Technical Report CS-TR-1425 Newcastle University"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2011.04.005"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576\u2013580 583","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0310-2"},{"key":"e_1_2_1_2_21_2","unstructured":"Jones CB (1981) Development methods for computer programs including a notion of interference. PhD thesis Oxford University. Printed as: Programming Research Group Technical Monograph 25"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00122417"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90011-6"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/44501.44503"},{"key":"e_1_2_1_2_27_2","unstructured":"Morgan CC (1994) Programming from specifications 2nd edn. Prentice Hall Upper Saddle River"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2003.09.002"},{"key":"e_1_2_1_2_29_2","unstructured":"Zhou C Hoare CAR (1981) Partial correctness of communication protocols. Technical Monograph PRG-20 Partial Correctness of Communicating Processes and Protocols. Oxford University Computing Laboratory pp 13\u201323"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Zhou C (1982) Weakest environment of communicating processes. In: Proc. of the June 7\u201310 1982 National Computer Conf. AFIPS \u201982 pp 679\u2013690 New York NY USA. ACM","DOI":"10.1145\/1500774.1500860"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0384-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0384-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0384-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0384-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T09:11:05Z","timestamp":1749028265000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0384-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11]]},"references-count":30,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2016,11]]}},"alternative-id":["10.1007\/s00165-016-0384-0"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0384-0","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,11]]},"assertion":[{"value":"22 April 2014","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 June 2016","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 July 2016","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}