{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:41Z","timestamp":1749124061969},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540627814"},{"type":"electronic","value":"9783540685173"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0030635","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T01:10:41Z","timestamp":1133399441000},"page":"697-711","source":"Crossref","is-referenced-by-count":8,"title":["Auxiliary variables and recursive procedures"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Schreiber","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,20]]},"reference":[{"key":"54_CR1","unstructured":"Peter Aczel. A system of proof rules for the correctness of iterative programs \u2014 some notational and organisational suggestions. Unpublished, August 1982."},{"issue":"2","key":"54_CR2","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/0890-5401(90)90037-I","volume":"84","author":"P. America","year":"1990","unstructured":"Pierre America and Frank de Boer. Proving total correctness of recursive procedures. Information and Computation, 84(2): 129\u2013162, 1990.","journal-title":"Information and Computation"},{"issue":"4","key":"54_CR3","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"K. R. Apt","year":"1981","unstructured":"Krzysztof R. Apt. Ten years of Hoare's logic: A survey \u2014 part I. ACM Transactions on Programming Languages and Systems, 3(4):431\u2013483, October 1981.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"4","key":"54_CR4","doi-asserted-by":"publisher","first-page":"665","DOI":"10.1137\/0209050","volume":"9","author":"K. R. Apt","year":"1980","unstructured":"Krzysztof R. Apt and Lambert G. L. T. Meertens. Completeness with finite systems of intermediate assertions for recursive program schemes. SIAM Journal on Computing, 9(4):665\u2013671, November 1980.","journal-title":"SIAM Journal on Computing"},{"issue":"1","key":"54_CR5","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1137\/0207005","volume":"7","author":"S. A. Cook","year":"1978","unstructured":"Stephen A. Cook. Soundness and completeness of an axiom system for program verification. SIAM Journal on Computing, 7(1):70\u201390, February 1978.","journal-title":"SIAM Journal on Computing"},{"key":"54_CR6","doi-asserted-by":"crossref","unstructured":"P. Cousot. Methods and logics for proving programs. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 15, pages 841\u2013993. Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50020-2"},{"key":"54_CR7","unstructured":"Ole-Johan Dahl. Verifiable Programming. International Series in Computer Science. Prentice Hall, 1992."},{"key":"54_CR8","doi-asserted-by":"crossref","unstructured":"R.W, Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Proc. Symp. in Applied Mathematics, volume 19, pages 19\u201332, 1967.","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"54_CR9","series-title":"number 15 in Workshops in Computing","first-page":"387","volume-title":"Current Trends in Hardware Verification and Automated Theorem Proving","author":"M. J. Gordon","year":"1991","unstructured":"Michael J.C. Gordon. Mechanizing programming logics in higher order logic. In G. Birtwhistle and P.A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving (Banff, Alberta), number 15 in Workshops in Computing, pages 387\u2013439. Springer, 1991."},{"key":"54_CR10","doi-asserted-by":"crossref","unstructured":"David Gries. The Science of Computer Programming, chapter 16, pages 193\u2013215. Springer, 1981.","DOI":"10.1007\/978-1-4612-5983-1_17"},{"key":"54_CR11","doi-asserted-by":"crossref","unstructured":"D. Harel. First-order Dynamic Logic, volume 68 of Lecture Notes in Computer Science. Springer, 1979.","DOI":"10.1007\/3-540-09237-4"},{"key":"54_CR12","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12:576\u2013580, 1969. Also in [14].","journal-title":"Communications of the ACM"},{"key":"54_CR13","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare. Procedures and parameters: An axiomatic approach. In E. Engeler, editor, Symposium on Semantics of Algorithmic Languages, volume 188 of Lecture Notes in Mathematics, pages 102\u2013116. Springer, 1971. Also in [14].","DOI":"10.1007\/BFb0059696"},{"key":"54_CR14","unstructured":"C.A.R. Hoare and Cliff B. Jones, editors. Essays in Computing Science. International Series in Computer Science. Prentice Hall, 1989."},{"key":"54_CR15","unstructured":"Cliff B. Jones. Systematic Software Development Using VDM. International Series in Computer Science. Prentice Hall, 2 edition, 1990."},{"key":"54_CR16","unstructured":"The Lego World Wide Web page. http:\/\/www.dcs.ed.ac.uk\/home\/lego."},{"key":"54_CR17","unstructured":"James H. Morris. Comments on \u201cprocedures and parameters\u201d. Undated and unpublished."},{"key":"54_CR18","first-page":"180","volume-title":"volume 1180 of Lecture Notes in Computer Science","author":"T. Nipkow","year":"1996","unstructured":"Tobias Nipkow. Winskel is (almost) right: Towards a mechanized semantics textbook. In V. Chandru and V. Vinay, editors, Proceedings of 16th Conference on Foundations of Software Technology and Theoretical Computer Science (Hyderabad, India, December 18\u201320, 1996), volume 1180 of Lecture Notes in Computer Science, pages 180\u2013192. Springer, 1996."},{"key":"54_CR19","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/0304-3975(83)90009-9","volume":"24","author":"E. Olderog","year":"1983","unstructured":"Ernst-R\u00fcdiger Olderog. On the notion of expressiveness and the rule of adaptation. Theoretical Computer Science, 24:337\u2013347, 1983.","journal-title":"Theoretical Computer Science"},{"key":"54_CR20","series-title":"volume 53 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"475","DOI":"10.1007\/3-540-08353-7_170","volume-title":"Sixth Mathematical Foundations of Computer Science","author":"S. Soko\u0142owski","year":"1977","unstructured":"Stefan Soko\u0142owski. Total correctness for procedures. In J. Gruska, editor, Sixth Mathematical Foundations of Computer Science (Tatransk\u00e1 Lomnica), volume 53 of Lecture Notes in Computer Science, pages 475\u2013483. Springer, 1977."}],"container-title":["Lecture Notes in Computer Science","TAPSOFT '97: Theory and Practice of Software Development"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0030635","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,8]],"date-time":"2019-04-08T10:56:25Z","timestamp":1554720985000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0030635"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540627814","9783540685173"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/bfb0030635","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}