{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:52:36Z","timestamp":1694623956601},"reference-count":14,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[1997,5,1]],"date-time":"1997-05-01T00:00:00Z","timestamp":862444800000},"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":[[1997,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            The temporal property \u2018to-always\u2019 has been proposed for specifying progress properties of concurrent programs. Although the \u2018to-always\u2019 properties are a subset of the \u2018leads-to\u2019 properties for a given program, \u2018to-always\u2019 has more convenient proof rules and in some cases more accurately describes the desired system behavior. In this paper, we give a predicate transformer\n            <jats:bold>wta<\/jats:bold>\n            , derive some of its properties, and use it to define \u2018to-always\u2019. Proof rules for \u2018to-always\u2019 are derived from the properties of\n            <jats:bold>wta<\/jats:bold>\n            . We conclude by briefly describing two application areas, nondeterministic data flow networks and self-stabilizing systems where \u2018to-always\u2019 properties are useful.\n          <\/jats:p>","DOI":"10.1007\/bf01211085","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T15:42:36Z","timestamp":1109346156000},"page":"270-282","source":"Crossref","is-referenced-by-count":3,"title":["A predicate transformer for the progress property \u2018to-always\u2019"],"prefix":"10.1145","volume":"9","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"}]},{"given":"Beverly A.","family":"Sanders","sequence":"additional","affiliation":[{"name":"Department of Computer and Information Science and Engineering, University of Florida, Gainesville, FL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.256850"},{"key":"e_1_2_1_2_2_2","unstructured":"Chandy K. M. Properties of parallel programs. Formal Aspects of Computing 1993."},{"key":"e_1_2_1_2_3_2","unstructured":"Chandy K. M 1994. Personal communication."},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Chandy K. M. and Misra J. Parallel Program Design: A Foundation . Addison-Wesley 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Chandy K. M. and Sanders B. A. Compositional specifications of parallel programs: Nondeterministic data flow. In Guy E. Blelloch K. Mani Chandy and Suresh Jagannathan editors Specification of Parallel Algorithms pages 51\u201364. DIMACS Series in Discrete Mathematics and Theoretical Computer Science American Mathematical Society 1994.","DOI":"10.1090\/dimacs\/018\/04"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00033-B"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Dijkstra E. W. and Scholten C. S. Predicate Calculus and Program Semantics . Springer-Verlag 1990.","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"e_1_2_1_2_8_2","unstructured":"Gouda M. May 1995. Personal communication."},{"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 Proceeding of the 8th ACM Symposium on Principles of Distributed Computing 1989.","DOI":"10.1145\/72981.72999"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Knapp E. A predicate transformer for progress. Information Processing Letters 33 1989\/90.","DOI":"10.1016\/0020-0190(90)90218-M"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Lamport L. win and sin : Predicate transformers for concurrency. ACM Transactions on Programming Languages and Systems 12(3) 1990.","DOI":"10.1145\/78969.78970"},{"issue":"2","key":"e_1_2_1_2_12_2","first-page":"273","article-title":"A logic for concurrent programming: Progress","volume":"3","author":"Misra J.","year":"1995","journal-title":"Journal of Computer and Software Engineering"},{"issue":"2","key":"e_1_2_1_2_13_2","first-page":"239","article-title":"A logic for concurrent programming: Safety","volume":"3","author":"Misra J.","year":"1995","journal-title":"Journal of Computer and Software Engineering"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Sanders B. A. Eliminating the substitution axiom from UNITY logic. Formal Aspects of Computing 3(2) 1991.","DOI":"10.1007\/BF01898402"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01211085.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01211085\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01211085","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:28:24Z","timestamp":1641482904000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01211085"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,5]]},"references-count":14,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1997,5]]}},"alternative-id":["10.1007\/BF01211085"],"URL":"https:\/\/doi.org\/10.1007\/bf01211085","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997,5]]}}}