{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:37:43Z","timestamp":1754483863406},"reference-count":15,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[1991,6,1]],"date-time":"1991-06-01T00:00:00Z","timestamp":675734400000},"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":[[1991,6]]},"abstract":"Abstract<\/jats:title>\n \n The UNITY substitution axiom, \u201cif (x=y) is an invariant of a program, then x can be replaced by y in any property of the program\u201d, is problematic for several reasons. In this paper, dual predicate transformers\n sst<\/jats:bold>\n and\n wst<\/jats:bold>\n are introduced that allow the strongest invariant of a program to be expressed, and these are used to give new definitions for the temporal operators\n unless<\/jats:italic>\n and\n ensures<\/jats:italic>\n . With the new definitions, the substitution\n axiom<\/jats:italic>\n is no longer needed, and can be replaced by a derived rule of inference which is formally justified in the logic. One important advantage is that the effects of the initial conditions on the properties of a program are formally captured in a convenient way, and one can forget about substitution in formal treatments of the UNITY proof system while still having it available when desirable to use during the derivation of programs. Composibility and completeness of the modified logic are also discussed.\n <\/jats:p>","DOI":"10.1007\/bf01898402","type":"journal-article","created":{"date-parts":[[2005,7,5]],"date-time":"2005-07-05T14:22:40Z","timestamp":1120573360000},"page":"189-205","source":"Crossref","is-referenced-by-count":63,"title":["Eliminating the substitution axiom from UNITY logic"],"prefix":"10.1145","volume":"3","author":[{"given":"Beverly A.","family":"Sanders","sequence":"first","affiliation":[{"name":"Institut f\u00fcr Computersysteme\/Departement Informatik, Swiss Federal Institute of Technology (ETH Z\u00fcrich), CH-8092, Z\u00fcrich, Switzerland"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_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_2_2","doi-asserted-by":"publisher","DOI":"10.1137\/0207005"},{"key":"e_1_2_1_2_3_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_4_2","doi-asserted-by":"crossref","unstructured":"Francez N.: Fairness Springer-Verlag 1986.","DOI":"10.1007\/978-1-4612-4886-6"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Gerth R. and Pnueli A.: Rooting UNITY. Proc. Fifth Int. Workshop on Software Specification and Design Pittsburgh Penn. 19\u201320 May 1989.","DOI":"10.1145\/75200.75202"},{"key":"e_1_2_1_2_6_2","unstructured":"Goldschlag D. M.: Mechanizing Unity. In: Proc. of IFIP Working Conf. on Programming Concepts and Methods Israel April 1990 M. Broy and C. B. Jones (eds) Elsevier Science Publishers B.V. 1990."},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Jutla C. S. Knapp E. and Rao J. R.: A Predicate Transformer Approach to Semantics of Parallel Programs. Proc. 8th Annual ACM Symp. on Principles of Distributed Computing 1989.","DOI":"10.1145\/72981.72999"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360251"},{"key":"e_1_2_1_2_9_2","unstructured":"Knapp E.: A Predicate Transformer for Progress. Information Processing Letters (to appear)."},{"key":"e_1_2_1_2_10_2","unstructured":"Lamport L: win and sin : Predicate Transformers for Concurrency. DEC SRC Technical Report 17 May 1987."},{"key":"e_1_2_1_2_11_2","unstructured":"Liu Z.: A Semantic Model for UNITY. University of Warwick Computer Science Technical Report RR144 August 1989."},{"key":"e_1_2_1_2_12_2","unstructured":"Misra J.: The Importance of Ensuring. Notes on UNITY: 11\u201390 11 January 1990."},{"key":"e_1_2_1_2_13_2","unstructured":"Misra J.: Soundness of the Substitution Axiom. Notes on UNITY: 14\u201390 2 March 1990."},{"key":"e_1_2_1_2_14_2","unstructured":"Sanders Beverly: Stepwise Refinement of Mixed Specifications of Concurrent Programs. In Proc. IFIP Working Conf. on Programming Concepts and Methods Israel April 1990 (M. Broy and C. B. Jones (eds) Elsevier Science Publishers B. V. 1990 1\u201325."},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01667079"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01898402.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01898402\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01898402","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:23:11Z","timestamp":1641482591000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01898402"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,6]]},"references-count":15,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1991,6]]}},"alternative-id":["10.1007\/BF01898402"],"URL":"https:\/\/doi.org\/10.1007\/bf01898402","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1991,6]]}}}