{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:51:58Z","timestamp":1694623918450},"reference-count":17,"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>Temporal weakest precondions are introduced for calculational reasoning about the states encountered during execution of not-necessarily terminating recursive procedures. The formalism can distinguish error from useful nontermination. The precondition functions are constructed in a new and more elegant way. Healthiness laws are discussed briefly. Proof rules are introduced that enable calculational proofs of various safety and progress properties. The construction of the precondition functions is justified in an Appendix that provides the operational semantics.<\/jats:p>","DOI":"10.1007\/bf01211215","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T22:18:16Z","timestamp":1109369896000},"page":"389-411","source":"Crossref","is-referenced-by-count":2,"title":["Safety and progress of recursive procedures"],"prefix":"10.1145","volume":"7","author":[{"given":"Wim H.","family":"Hesselink","sequence":"first","affiliation":[{"name":"Department of Computing Science, Rijksuniversiteit Groningen, Groningen, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","first-page":"42","volume-title":"Stepwise Refinement of Distributed Systems","author":"Back R. J. R.","year":"1990"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Bijlsma A.: Semantics of quasi-boolean expressions. In: W.H.J. Feijen et al. (eds.): Beauty is our business a birthday salute to Edsger W. Dijkstra. Springer. 1990 pp. 27\u201335.","DOI":"10.1007\/978-1-4612-4476-9_4"},{"key":"e_1_2_1_2_3_2","unstructured":"Dijkstra E. W.: A discipline of programming. Prentice-Hall 1976."},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Dijkstra E. W. and Scholten C. S.: Predicate calculus and program semantics. Springer. 1990.","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90142-9"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Hesselink W. H.: Programs Recursion and Unbounded Choice predicate transformation semantics and transformation rules. Cambridge University Press 1992.","DOI":"10.1017\/CBO9780511569784"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211249"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)00016-K"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Hesselink W. H. and Reinds R.: Temporal preconditions of recursive procedures. In: J.W. de Bakker W.-P. de Roever G. Rozenberg (eds.): Semantics: Foundations and Applications. Proceedings of REX Workshop Beekbergen 1992. Springer Verlag 1993 (LNCS 666) pp. 236\u2013260.","DOI":"10.1007\/3-540-56596-5_36"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Hoare C. A. R.: Procedures and parameters: an axiomatic approach. In: Symposium on Semantics of Algorithmic Languages. (ed. E. Engeler) Springer Verlag (Lecture Notes in Math. 188) 1971 pp. 102\u2013116.","DOI":"10.1007\/BFb0059696"},{"key":"e_1_2_1_2_11_2","unstructured":"Lukkien J. J.: Parallel Program Design and Generalized Weakest Preconditions. Thesis Groningen 1991."},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01212336"},{"key":"e_1_2_1_2_13_2","unstructured":"Morgan C.: Programming from Specifications. Prentice Hall 1990."},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.5555\/79245.79246"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90011-6"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.5555\/77693.77694"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","first-page":"472","DOI":"10.1007\/3-540-07854-1_217","volume-title":"Mathematical Foundations of Computer Science 1976","author":"de Roever W. P.","year":"1976"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01211215.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01211215\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01211215","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:24:51Z","timestamp":1641482691000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01211215"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,7]]},"references-count":17,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1995,7]]}},"alternative-id":["10.1007\/BF01211215"],"URL":"https:\/\/doi.org\/10.1007\/bf01211215","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,7]]}}}