{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:38:03Z","timestamp":1725511083616},"reference-count":14,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[1995,7,1]],"date-time":"1995-07-01T00:00:00Z","timestamp":804556800000},"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":[[1995,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>The \u2018programming\u2019 language DUALITY is presented and its utility for the description and analysis of UNITY is demonstrated. DUALITY is a simple language supporting demonic and angelic choice and two forms of tail-recursion. Starting from the predicate transformer semantics that was developed by C.S. Jutla, E. Knapp, and J.R. Rao for UNITY, we show that, given a UNITY program, we can write a program in DUALITY that has the same formal characteristics. This we use to reformulate and reprove some important theorems from the UNITY theory, viz. the \u2018PSP-rule\u2019 and the \u2018completion rule\u2019. Finally we show that the predicate transformers proposed by K.M. Chandy and B.A. Sanders for reasoning about concurrent computation also fit nicely within this framework.<\/jats:p>","DOI":"10.1007\/bf01211214","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T22:18:16Z","timestamp":1109369896000},"page":"353-388","source":"Crossref","is-referenced-by-count":8,"title":["DUALITY: A simple formalism for the analysis of UNITY"],"prefix":"10.1145","volume":"7","author":[{"given":"Rutger M.","family":"Dijkstra","sequence":"first","affiliation":[{"name":"Department of Computing Science, University of Groningen, PO Box 800, 9700, AV Groningen, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Backhouse R. and van der Woude J.: A relational theory of datatypes. In: Lecture Notes of the STOP 1992 Summerschool on Constructive Algorithmics.","DOI":"10.1007\/3-540-57499-9_15"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00259469"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Chandy K.M. and Misra J.: Parallel Program Design a foundation . Addison-Wesley 1990.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"e_1_2_1_2_4_2","unstructured":"Chandy K.M. and Sanders B.A.: Conjunctive predicate transformers for reasoning about concurrent computation. to appear in: the Science of Computer Programming."},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Dijkstra E.W. and Scholten C.S.: Predicate Calculus and Program Semantics . Texts and Monographs in Computer Science. Springer Verlag New York Inc. 1990.","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Hesselink W.H.: Programs Recursion and Unbounded Choice . Cambridge Tracts in Theoretical Computer Science. Cambridge University Press 1992.","DOI":"10.1017\/CBO9780511569784"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)00016-K"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Hesselink W.H. and Reinds R.: Temporal preconditions of recursive procedures. In W.P. de Roever J.W. de Bakker and G. Rozenberger editors Semantics: Foundations and Applications pages 236\u2013260. Springer-Verlag 1992.","DOI":"10.1007\/3-540-56596-5_36"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Jutla C. S. Knapp E. and Rao J. R.: A predicate transformer approach to semantics of parallel programs. In Proceedings of the 8th Annual ACM symposium on Principles of Distributed Computing pages 249\u2013263. ACM Press 1989.","DOI":"10.1145\/72981.72999"},{"key":"e_1_2_1_2_10_2","volume-title":"PhD thesis","author":"Knapp E.","year":"1990"},{"key":"e_1_2_1_2_11_2","volume-title":"PhD thesis","author":"Lukkien J.J.","year":"1990"},{"key":"e_1_2_1_2_12_2","unstructured":"Misra J. Soundness of the substitution axiom. Notes on UNITY: 14\u201390 March 1990."},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01898402"},{"key":"e_1_2_1_2_14_2","unstructured":"van de Snepscheut J.L.A.: Is UNITY consistent? internet newsgroup comp.theory."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01211214.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01211214\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01211214","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:24:46Z","timestamp":1641482686000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01211214"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,7]]},"references-count":14,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1995,7]]}},"alternative-id":["10.1007\/BF01211214"],"URL":"https:\/\/doi.org\/10.1007\/bf01211214","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,7]]}}}