{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T08:45:33Z","timestamp":1773996333054,"version":"3.50.1"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2017,9,1]],"date-time":"2017-09-01T00:00:00Z","timestamp":1504224000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,9,1]],"date-time":"2017-09-01T00:00:00Z","timestamp":1504224000000},"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":[[2017,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            A wide-spectrum language integrates specification constructs into a programming language in a manner that treats a specification command just like any other command. The primary contribution of this paper is a semantic model for a wide-spectrum language that supports concurrency and a refinement calculus. A distinguishing feature of the language is that steps of the environment are modelled explicitly, alongside steps of the program. From these two types of steps a rich set of specification commands can be constructed, based on operators for nondeterministic choice, and sequential and parallel composition. We also introduce a novel operator,\n            <jats:italic>weak conjunction<\/jats:italic>\n            , which is used extensively to conjoin separate aspects of specifications, allowing us to take a separation-of-concerns approach to subsequent reasoning. We provide a denotational semantics for the language based on traces, which may be terminating, aborting, infeasible, or infinite. To demonstrate the generality and unifying strength of the language, we use it to express a range of concepts from the concurrency literature, including: a refinement theory for rely\/guarantee reasoning; an abstract specification of local variables in a concurrent context; specification of an abstract, linearisable data structure; a partial encoding of temporal logic; and defining the relationships between notions of nonblocking programs. The novelty of the paper is that these diverse concepts build on the same theory. In particular, the\n            <jats:italic>rely<\/jats:italic>\n            concept from Jones\u2019 rely\/guarantee framework, and a stronger\n            <jats:italic>demand<\/jats:italic>\n            concept that restricts the environment, are reused across the different domains to express assumptions about the environment. The language and model form an instance of an abstract concurrent program algebra, and this facilitates reasoning about properties of the model at a high level of abstraction.\n          <\/jats:p>","DOI":"10.1007\/s00165-017-0416-4","type":"journal-article","created":{"date-parts":[[2017,2,27]],"date-time":"2017-02-27T09:07:22Z","timestamp":1488186442000},"page":"853-875","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["Designing a semantic model for a wide-spectrum language with concurrency"],"prefix":"10.1145","volume":"29","author":[{"given":"Robert J.","family":"Colvin","sequence":"first","affiliation":[{"name":"School of Information Technology and Electrical Engineering, The University of Queensland, 4072, Brisbane, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3649-392X","authenticated-orcid":false,"given":"Ian J.","family":"Hayes","sequence":"additional","affiliation":[{"name":"School of Information Technology and Electrical Engineering, The University of Queensland, 4072, Brisbane, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Larissa A.","family":"Meinicke","sequence":"additional","affiliation":[{"name":"School of Information Technology and Electrical Engineering, The University of Queensland, 4072, Brisbane, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_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_2_2","doi-asserted-by":"crossref","unstructured":"Back R-JR (1989) A method for refining atomicity in parallel algorithms. In: Odijk E Rem M Syre J-C (eds) PARLE\u201989 parallel architectures and languages Europe. LNCS vol 366. Springer Berlin pp 199\u2013216","DOI":"10.1007\/3-540-51285-3_42"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Back R-JR von Wright J (1998) Refinement calculus: a systematic introduction. Springer New York","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0056"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.034"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exm030"},{"key":"e_1_2_1_2_7_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) FM\u201999\u2014Formal Methods. Lecture Notes in Computer Science vol 1709. Springer Berlin pp 1245\u20131265","DOI":"10.1007\/3-540-48118-4_16"},{"key":"e_1_2_1_2_8_2","volume-title":"Concurrency verification: introduction to compositional and noncompositional methods","author":"De Roever W-P","year":"2001"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200032"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Dongol B (2006) Formalising progress properties of non-blocking programs. In: Liu Z He J (eds) Formal Methods and Software Engineering. Lecture Notes in Computer Science vol 4260. Springer Berlin pp 284\u2013303","DOI":"10.1007\/11901433_16"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"#cr-split#-e_1_2_1_2_12_2.1","doi-asserted-by":"crossref","unstructured":"Foster S Zeyda F Woodcock J (2014) Isabelle\/UTP: a mechanised theory engineering framework. In: Naumann D","DOI":"10.1007\/978-3-319-14806-9_2"},{"key":"#cr-split#-e_1_2_1_2_12_2.2","unstructured":"(ed) Unifying Theories of Programming-5th International Symposium UTP 2014 Singapore May 13 2014 Revised Selected Papers. Lecture Notes in Computer Science vol 8963. Springer pp 21-41"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-016-0384-0"},{"key":"e_1_2_1_2_14_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_15_2","doi-asserted-by":"crossref","unstructured":"Hayes IJ Utting M (1998) Deadlines are termination. In: Gries D De Roever W-P (eds) IFIP TC2\/WG2.2 2.3 International Conference on Programming Concepts and Methods (PROCOMET\u201998). Chapman and Hall London pp 186\u2013204","DOI":"10.1007\/978-0-387-35358-6_15"},{"key":"e_1_2_1_2_16_2","unstructured":"Hayes I (ed) (1993) Specification case studies 2nd edn. Prentice Hall International Englewood Cliffs"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Hayes IJ Meinicke L (2014) Invariants well-founded statements and real-time program algebra. In: Jones CB Pihlajasaari P Sun J (eds) Formal Methods (FM 2014). LNCS vol 8442. Springer Berlin pp 318\u2013334","DOI":"10.1007\/978-3-319-06410-9_23"},{"key":"e_1_2_1_2_18_2","unstructured":"Herlihy M Luchangco V Moir M (2003) Obstruction-free synchronization: double-ended queues as an example. In: ICDCS\u201903: Proceedings of the 23rd International Conference on Distributed Computing Systems Washington DC USA. IEEE Computer Society pp 522\u2013529"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_1_2_20_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_21_2","doi-asserted-by":"publisher","DOI":"10.5555\/3921"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2011.04.005"},{"key":"e_1_2_1_2_23_2","unstructured":"Jones CB (1981) Development methods for computer programs including a notion of interference. PhD thesis Oxford University. Oxford University Computing Laboratory (now Computer Science) Technical Monograph PRG-25"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0310-2"},{"key":"e_1_2_1_2_26_2","unstructured":"Lamport L (2003) Specifying systems: the TLA+ language and tools for hardware and software engineers. Addison Wesley Reading"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/44501.44503"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Plotkin GD (2004) A structural approach to operational semantics. J Log Algebr Program 60\u201361:17\u2013139","DOI":"10.1016\/j.jlap.2004.05.001"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science. IEEE pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_2_30_2","volume-title":"The Z notation: a reference manual","author":"Spivey JM","year":"1992","edition":"2"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2003.09.002"},{"key":"e_1_2_1_2_32_2","volume-title":"Using Z: specification, refinement, and proof","author":"Woodcock J","year":"1996"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-017-0416-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0416-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0416-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-017-0416-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,7]],"date-time":"2022-01-07T06:55:03Z","timestamp":1641538503000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-017-0416-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9]]},"references-count":33,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2017,9]]}},"alternative-id":["10.1007\/s00165-017-0416-4"],"URL":"https:\/\/doi.org\/10.1007\/s00165-017-0416-4","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,9]]},"assertion":[{"value":"23 March 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 November 2016","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 February 2017","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}