{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:52:58Z","timestamp":1694623978010},"reference-count":10,"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>A relational framework which unifies Hoare's logic and VDM is presented. Within this framework a partial correctness version of VDM is defined. It is argued that this partial correctness version of VDM is intuitive and consistent with the original total correctness version. Furthermore it is shown how both partial and total correctness formulae and specifications can be translated from Hoare's logic into VDM and vice versa. VDM's satisfiability requirement is briefly discussed, and a similar condition for Hoare's logic is defined.:<\/jats:p>","DOI":"10.1007\/bf01214625","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T16:30:35Z","timestamp":1109349035000},"page":"91-105","source":"Crossref","is-referenced-by-count":0,"title":["Hoare's logic and VDM"],"prefix":"10.1145","volume":"7","author":[{"given":"J.","family":"Coenen","sequence":"first","affiliation":[{"name":"Department of Mathematics and Computing Science, Eindhoven University of Technology, PO Box 513, 5600, MB Eindhoven, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1145\/357146.357150","article-title":"Ten Years of Hoare's Logic: A Survey \u2014 Part I","volume":"4","author":"Apt K. R.","year":"1981","journal-title":"ACM TOPLAS"},{"key":"e_1_2_1_2_2_2","unstructured":"Bakker J. W. de: Mathematical Theory of Program Correctness . Prentice-Hall 1980."},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Coenen J. Roever W.-P. de Zwiers J.: Assertional Data Reification Proofs: Survey and Perspective. Proc. 4th BCS-FACS Refinement Workshop pp. 97\u2013114 Workshops in Computing Springer-Verlag 1991.","DOI":"10.1007\/978-1-4471-3756-6_5"},{"key":"e_1_2_1_2_4_2","unstructured":"Gorelick G. A.: A Complete Axiomatic System for Proving Assertions about Recursive and Non-Recursive Programs. Tech. Report No. 75 Dept. of Computer Science University of Toronto 1975."},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Hoare C. A. R.: Procedures and Parameters: An Axiomatic Approach. Symp. on Semantics of Algorithmic Languages pp. 102\u2013116 LNM 188 Springer-Verlag 1971.","DOI":"10.1007\/BFb0059696"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Jones C. B.: VDM Proof Obligations and their Justification. Proc. VDM-Europe Symposium pp. 260\u2013286 LNCS 252 Springer-Verlag 1987.","DOI":"10.1007\/3-540-17654-3_15"},{"key":"e_1_2_1_2_8_2","unstructured":"Jones C. B.: Systematic Software Development Using VDM (second edition). Prentice-Hall 1990."},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90009-9"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90048-X"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01214625.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01214625\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01214625","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:22:12Z","timestamp":1641482532000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01214625"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,1]]},"references-count":10,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1995,1]]}},"alternative-id":["10.1007\/BF01214625"],"URL":"https:\/\/doi.org\/10.1007\/bf01214625","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,1]]}}}