{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,2]],"date-time":"2025-09-02T10:37:30Z","timestamp":1756809450467},"reference-count":16,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"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,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Although many programming languages contain exception handling mechanisms, their formal treatment \u2014 necessary for rigorous development \u2014 can be complex. Nevertheless, this paper presents a simple incorporation of\n            <jats:bold>exit<\/jats:bold>\n            commands and exception blocks into a rigorous program development method. The refinement calculus, chosen for the exercise, is a method of developing imperative programs. It is based on weakest preconditions, although they are not used explicitly during program construction; they merely justify the general method. In the style of the refinement calculus, program development laws are given that introduce and allow the manipulation of\n            <jats:bold>exit<\/jats:bold>\n            s. The soundness of the new laws is shown using weakest preconditions (as for the existing refinement calculus laws). The extension of weakest preconditions needed to handle\n            <jats:bold>exit<\/jats:bold>\n            s is a variation on earlier work of Cristian; the variation is necessary to handle nondeterminism.\n          <\/jats:p>","DOI":"10.1007\/bf01214623","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T16:30:35Z","timestamp":1109349035000},"page":"54-76","source":"Crossref","is-referenced-by-count":8,"title":["Exits in the refinement calculus"],"prefix":"10.1145","volume":"7","author":[{"given":"Steve","family":"King","sequence":"first","affiliation":[{"name":"Programming Research Group, Oxford University Computing Laboratory, Wolfson Building, Parks Rd, OX1 3QD, Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carroll","family":"Morgan","sequence":"additional","affiliation":[{"name":"Programming Research Group, Oxford University Computing Laboratory, Wolfson Building, Parks Rd, OX1 3QD, Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","volume-title":"Tract 131","author":"Back R.-J. R.","year":"1980"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00291051"},{"key":"e_1_2_1_2_3_2","unstructured":"Back R.-J. R. and Karttunen M.: A predicate transformer semantics for statements with multiple exits. University of Helsinki unpublished MS 1983."},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1984.5010218"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_1_2_6_2","volume-title":"A Discipline of Programming","author":"Dijkstra E. W.","year":"1976"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Lukkien J. J.: An operational semantics for the guarded command language. In R. Bird C.C. Morgan and J.C.P. Woodcock editors Mathematics of Program Construction number 669 in Lecture Notes in Computer Science. Springer-Verlag 1992.","DOI":"10.1007\/3-540-56625-2_16"},{"key":"e_1_2_1_2_9_2","unstructured":"Leino K. R. M. and van de Snepscheut J. L. A.: Semantics of exceptions. Technical Report Caltech-CS-TR-93-94 Computer Science Department California Institute of Technology 1993."},{"key":"e_1_2_1_2_10_2","unstructured":"Manasse M. S. and Nelson C. G.: Correct compilation of control structures. Technical report AT&T Bell Laboratories September 1984."},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90011-6"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Morgan C. C.: The specification statement. Trans. Prog. Lang. Sys. 10(3) July 1988. Reprinted in [MoV93].","DOI":"10.1145\/44501.44503"},{"key":"e_1_2_1_2_13_2","volume-title":"Programming from Specifications","author":"Morgan C. C.","year":"1994","edition":"2"},{"key":"e_1_2_1_2_14_2","unstructured":"Morgan C. C. and Vickers T. N.: editors. On the Refinement Calculus . FACIT Series in Computer Science. Springer 1993."},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/69558.69559"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(90)90056-J"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01214623.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01214623\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01214623","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:21:59Z","timestamp":1641482519000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01214623"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,1]]},"references-count":16,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1995,1]]}},"alternative-id":["10.1007\/BF01214623"],"URL":"https:\/\/doi.org\/10.1007\/bf01214623","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,1]]}}}