{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:52:50Z","timestamp":1725663170666},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540100034"},{"type":"electronic","value":"9783540393467"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1980]]},"DOI":"10.1007\/3-540-10003-2_84","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T17:00:20Z","timestamp":1330189220000},"page":"363-373","source":"Crossref","is-referenced-by-count":18,"title":["Present-day Hoare-like systems for programming languages with procedures: Power, limits and most likely extensions"],"prefix":"10.1007","author":[{"given":"Hans","family":"Langmaack","sequence":"first","affiliation":[]},{"given":"Ernst-R\u00fcdiger","family":"Olderog","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,24]]},"reference":[{"key":"31_CR1","unstructured":"Apt, K.R.: A sound and complete Hoare-like system for a fragment of PASCAL, Math. Centrum IW 96\/78, Amsterdam, 59 pp. (1978)"},{"key":"31_CR2","unstructured":"Apt, K.R.: Ten years of Hoare's logic, a survey, Fac.Econom., Erasmus Univ. Rotterdam, 43 pp. (1979)"},{"key":"31_CR3","doi-asserted-by":"crossref","unstructured":"Cartwright, R., Oppen, D.: Unrestricted procedure calls in Hoare's logic, in: Proc. 5th Annual ACM Symposium on Principles of Programming Languages, 131\u2013140 (1978)","DOI":"10.1145\/512760.512774"},{"issue":"1","key":"31_CR4","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1145\/322108.322121","volume":"26","author":"E. M. Clarke Jr.","year":"1979","unstructured":"Clarke, E.M. Jr.: Programming Language constructs for which it is impossible to obtain good Hoare axiom systems, J.ACM 26, 1, 129\u2013147 (1979)","journal-title":"J.ACM"},{"key":"31_CR5","unstructured":"Clarke, E.M. Jr.: Private letter (1979)"},{"issue":"1","key":"31_CR6","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1137\/0207005","volume":"7","author":"S. A. Cook","year":"1978","unstructured":"Cook, S.A.: Soundness and completeness of an axiomatic system for program verification. SIAM. J. Comp. 7, 1, 70\u201390 (1978)","journal-title":"SIAM. J. Comp."},{"key":"31_CR7","unstructured":"Damm, W., Fehr, E.: On the power of selfapplication and higher type recursion, in: Aussiello, G., B\u00f6hm, C. (Ed.): Automata Languages and Programming, 5th Colloquium; Udine, July 1978, 177\u2013191 (1979)"},{"issue":"8","key":"31_CR8","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E. W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, non-determinacy and formal derivation of programs, Comm. ACM 18, 8, 453\u2013457 (1975)","journal-title":"Comm. ACM"},{"key":"31_CR9","unstructured":"Donahue, J.E.: Complementary definitions of programming language semantics, Springer Lecture Notes in Computer Science 42, 172 pp. (1976)"},{"key":"31_CR10","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1145\/321371.321385","volume":"14","author":"S. Ginsburg","year":"1967","unstructured":"Ginsburg, S., Greibach, S.A., Harrison, M.A.: Stack automata and compiling, J. ACM 14, 172\u2013201 (1967)","journal-title":"J. ACM"},{"key":"31_CR11","volume-title":"A complete axiomatic system for proving assertions about recursive and non-recursive programs","author":"G. A. Gorelick","year":"1975","unstructured":"Gorelick, G.A.: A complete axiomatic system for proving assertions about recursive and non-recursive programs. Tech. Rep. 75, Dept. Comp. Sc. Univ. Toronto (1975)"},{"key":"31_CR12","doi-asserted-by":"crossref","unstructured":"Harel, D.: First-order dynamic logic. Springer Lecture Notes in Computer Science 68, 133 pp. (1979)","DOI":"10.1007\/3-540-09237-4"},{"key":"31_CR13","doi-asserted-by":"crossref","unstructured":"Harel, D., Pnueli, A., Stavi, J.: A complete axiomatic system for proving deductions about recursive programs, in: Proc. 9th ACM Symposium on Theory of Computing, 249\u2013260 (1977)","DOI":"10.1145\/800105.803415"},{"issue":"583","key":"31_CR14","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C. A. R. R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming, Comm. ACM 12, 576\u2013580, 583 (1969)","journal-title":"Comm. ACM"},{"key":"31_CR15","unstructured":"Hoare, C.A.R.: Procedures and parameters: An axiomatic approach, in: Engeler, E. (Ed.): Symposium on Algorithmic Languages, Springer Lecture Notes in Mathematics 188, 102\u2013116 (1971)"},{"key":"31_CR16","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/BF00288746","volume":"4","author":"S. Igarashi","year":"1975","unstructured":"Igarashi, S., London, R.L. Luckham, D.C.: Automatic program verification I: A logical basis and its implementation. Acta Informatica 4, 145\u2013182 (1975)","journal-title":"Acta Informatica"},{"key":"31_CR17","volume-title":"PASCAL user manual and report","author":"K. Jensen","year":"1975","unstructured":"Jensen, K., Wirth, N.: PASCAL user manual and report. Springer, New York \u2014 Heidelberg \u2014 Berlin (1975)"},{"key":"31_CR18","doi-asserted-by":"crossref","unstructured":"Kandzia, P.: On the \"most recent\" property of ALGOL-like programs, in: Springer Lecture Notes in Computer Science 14, Ed. J. Loeckx, 97\u2013111 (1974)","DOI":"10.1007\/978-3-662-21545-6_7"},{"key":"31_CR19","unstructured":"Klein, H.-J.: Untersuchungen im Zusammenhang mit der \"most recent\" Eigenschaft von Programmen. Bericht Nr. 8\/77, Inst. Inform. Prakt.Math.Univ. Kiel, 41 pp. (1977)"},{"key":"31_CR20","first-page":"110","volume":"2","author":"H. Langmaack","year":"1973","unstructured":"Langmaack, H.: On correct procedure parameter transmission in higher programming languages. Acta Informatica 2, 110\u2013142 (1973)","journal-title":"Acta Informatica"},{"key":"31_CR21","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1007\/BF00289503","volume":"2","author":"H. Langmaack","year":"1973","unstructured":"Langmaack, H.: On procedures as open subroutines I, II. Acta Informatica 2, 311\u2013333 (1973) and Acta Informatica 3, 227\u2013241 (1974)","journal-title":"Acta Informatica"},{"key":"31_CR22","doi-asserted-by":"crossref","unstructured":"Langmaack, H.: On a theory of decision problems in programming languages, in: Blum, E.K., Takasu, S. (Ed.): Proceed. Internat. Conf. Math. Studies Information Processing, Kyoto 1978, Springer Lecture Notes in Computer Science 75, 538\u2013558 (1979)","DOI":"10.1007\/3-540-09541-1_38"},{"key":"31_CR23","unstructured":"Langmaack, H.: On termination problems for finitely interpreted ALGOL-like programs. Bericht Nr. 7904, Inst. Inf. Prakt. Math. Univ. Kiel, 42 pp. (1979)"},{"key":"31_CR24","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1016\/0020-0190(79)90058-9","volume":"9","author":"H. Langmaack","year":"1979","unstructured":"Langmaack, H., Lippe, W.M., Wagner, F.: The formal termination problem for programs with finite ALGOL 68-modes. Inf.Proc. Letters 9, 155\u2013159 (1979)","journal-title":"Inf.Proc. Letters"},{"key":"31_CR25","unstructured":"Lippe, W.M., Simon, F.: A formal notion for equivalence of ALGOL-like programs, in: Proceedings of the 3rd International Symposium on Programming in Paris: Program Transformation, ed. by B. Robinet, Dunod-Paris, 141\u2013158 (1978)"},{"key":"31_CR26","doi-asserted-by":"crossref","unstructured":"Lipton, R.J.: A necessary and sufficient condition for the existence of Hoare logics, in: 18th Symp. on Found. Comp. Science, ed. IEEE, 1\u20136 (1977)","DOI":"10.1109\/SFCS.1977.1"},{"issue":"1","key":"31_CR27","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1145\/942578.807085","volume":"7","author":"C. L. McGowan","year":"1972","unstructured":"McGowan, C.L.: The \"most recent\" error: its causes and correction. SIGPLAN Notices 7, 1, 191\u2013202 (1972)","journal-title":"SIGPLAN Notices"},{"key":"31_CR28","first-page":"420","volume":"4","author":"P. Naur","year":"1963","unstructured":"Naur, P. (ed.), et al.: Report on the algorithmic language ALGOL 60, Numer. Math. 4, 420\u2013453 (1963)","journal-title":"Numer. Math."},{"key":"31_CR29","unstructured":"Olderog, E.-R.: Sound and complete Hoare-like calculi based on copy rules. Bericht 7905, Inst. Inf. Prakt. Math. Univ. Kiel, 57 pp. (1979); submitted for publication"},{"key":"31_CR30","unstructured":"in preparation"},{"key":"31_CR31","unstructured":"Prawitz, D.: Natural deduction \u2014 a proof-theoretic study. Stockholm, Almquist & Wiksell 1965"},{"key":"31_CR32","unstructured":"Wijngaarden, A. van, et al. (Ed.): Revised report on the algorithmic language ALGOL 68, Acta Informatica 5, 1\u2013236 (1975)"},{"key":"31_CR33","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1145\/322047.322062","volume":"25","author":"M. Wand","year":"1978","unstructured":"Wand, M.: A new incompleteness result for Hoare's system. J. ACM 25, 168\u2013175 (1978)","journal-title":"J. ACM"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-10003-2_84.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:02:23Z","timestamp":1605643343000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-10003-2_84"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1980]]},"ISBN":["9783540100034","9783540393467"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-10003-2_84","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1980]]}}}