{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:21:46Z","timestamp":1725456106238},"publisher-location":"Berlin\/Heidelberg","reference-count":22,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354011212X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0025790","type":"book-chapter","created":{"date-parts":[[2005,11,19]],"date-time":"2005-11-19T05:23:41Z","timestamp":1132377821000},"page":"349-374","source":"Crossref","is-referenced-by-count":0,"title":["A critique of the foundations of Hoare-style programming logics"],"prefix":"10.1007","author":[{"given":"Michael J.","family":"O'Donnell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-6272-5","volume-title":"The Design of Well-Structured and Correct Programs","author":"S. Alagi\u0107","year":"1978","unstructured":"Alagi\u0107, S. and Arbib, M.A. The Design of Well-Structured and Correct Programs. Springer-Verlag, New York, (1978)."},{"key":"21_CR2","volume-title":"A sound and complete Hoare-like system for a fragment of Pascal. Report IW\/78","author":"K.R. Apt","year":"1978","unstructured":"Apt, K.R. A sound and complete Hoare-like system for a fragment of Pascal. Report IW\/78, Mathematisch Centrum, Afdeling Informatica, Amsterdam, (1978)."},{"issue":"2","key":"21_CR3","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/BF00264021","volume":"11","author":"M.A. Arbib","year":"1979","unstructured":"Arbib, M.A. and Alagi\u0107, S. Proof rules for gotos. Acta Informatica 11.2, (1979), 139\u2013148.","journal-title":"Acta Informatica"},{"issue":"3","key":"21_CR4","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/BF00288660","volume":"6","author":"E.A. Ashcroft","year":"1976","unstructured":"Ashcroft, E.A., Clint M. and Hoare, C.A.R. Remarks on program proving: jumps and functions, Acta Informatica 6:3 (1976), 317.","journal-title":"Acta Informatica"},{"issue":"1","key":"21_CR5","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1145\/322108.322121","volume":"26","author":"E.M. Clarke","year":"1979","unstructured":"Clarke, E.M. Programming language constructs for which it is impossible to obtain good Hoare-like axiom systems, JACM 26:1, (1979), 129\u2013147.","journal-title":"JACM"},{"issue":"3","key":"21_CR6","first-page":"214","volume":"1","author":"M. Clint","year":"1972","unstructured":"Clint, M. and Hoare, C.A.R. Program proving: jumps and functions Acta Informatica 1:3 (1972), 214\u2013224.","journal-title":"Program proving: jumps and functions Acta Informatica"},{"key":"21_CR7","volume-title":"A Programming Logic","author":"R. Constable","year":"1978","unstructured":"Constable, R. and O'Donnell, M. A Programming Logic. Winthrop, Cambridge Massachusetts, (1978)."},{"issue":"1","key":"21_CR8","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1137\/0207005","volume":"7","author":"S.A. Cook","year":"1978","unstructured":"Cook, S.A. Soundness and completeness of an axiom system for program verification. SIAM Journal on Computing 7:1 (1978), 70\u201390.","journal-title":"SIAM Journal on Computing"},{"key":"21_CR9","volume-title":"Goto Statements. Chapter 10 of Mathematical Theory of Program Correctness by J. de Bakker","author":"A. Bruin de","year":"1980","unstructured":"de Bruin, A. Goto Statements. Chapter 10 of Mathematical Theory of Program Correctness by J. de Bakker. Prentice\/Hall International, Englewood Cliffs, NJ, (1980)."},{"issue":"8","key":"21_CR10","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, nondeterminacy and formal derivation of programs. CACM 18:8, (1975), 453\u2013457.","journal-title":"CACM"},{"key":"21_CR11","series-title":"Lecture notes in Computer Science","volume-title":"Complementary Definitions of Programming Language Semantics","author":"J.E. Donahue","year":"1976","unstructured":"Donahue, J.E. Complementary Definitions of Programming Language Semantics. Lecture notes in Computer Science 42, Springer-Verlag, New York, (1976)."},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Floyd, R.W. Assigning meanings to programs. Proceedings of symposia in applied mathematics, 19, American Mathematical Society, Providence, (1967).","DOI":"10.1090\/psapm\/019\/0235771"},{"issue":"10","key":"21_CR13","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R. An axiomatic basis for computer programming. CACM 12:10, (1969), 576\u2013580.","journal-title":"CACM"},{"issue":"4","key":"21_CR14","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/BF00289504","volume":"2","author":"C.A.R. Hoare","year":"1973","unstructured":"Hoare, C.A.R. and Wirth, N. An axiomatic definition of the programming language PASCAL. Acta Informatica 2:4, (1973), 335\u2013355.","journal-title":"Acta Informatica"},{"issue":"4","key":"21_CR15","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/BF00289468","volume":"7","author":"T. Kowaltowski","year":"1977","unstructured":"Kowaltowski, T. Axiomatic approach to side effects and general jumps. Acta Informatica 7:4, (1977), 357\u2013360.","journal-title":"Acta Informatica"},{"issue":"1","key":"21_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF00260921","volume":"10","author":"R.L. London","year":"1978","unstructured":"London, R.L., Guttag, J.V., Horning, J.J., Lampson, B.W., Mitchell, J.G., and Popek, G.J. Proof rules for the programming language Euclid. Acta Informatica 10:1, (1978), 1\u201326.","journal-title":"Acta Informatica"},{"key":"21_CR17","unstructured":"Manna, Z. and Waldinger, R. Is \"sometime\" sometimes better than \"always\"? Second international conference on Software Engineering, (1976)."},{"key":"21_CR18","unstructured":"Mendelson, E. Introduction to Mathematical Logic. 2nd edition, Van Nostrand, N.Y., (1976)."},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Musser, D. A proof rule for functions. USC information sciences institute technical report ISI\/RR-77-62, (1977).","DOI":"10.21236\/ADA046298"},{"key":"21_CR20","unstructured":"Olderog, E. Sound and complete Hoare-like calculi based on copy rules. Technical report 7905, Christian-Albrechts Universitat, Kiel, (1979)."},{"key":"21_CR21","first-page":"124","volume-title":"From Frege to Godel: A Source Book in Mathematical Logic, 1879\u20131931","author":"B. Russell","year":"1967","unstructured":"Russell, B. Letter to G. Frege, June 16, 1902. From Frege to Godel: A Source Book in Mathematical Logic, 1879\u20131931. J. van Heijenoort (Ed.), Harvard University Press, Cambridge, (1967), 124\u2013125."},{"key":"21_CR22","first-page":"19","volume-title":"Computers and Automata","author":"D. Scott","year":"1972","unstructured":"Scott, D. and Strachey, C. Towards a mathematical semantics for computer languages. Computers and Automata. J. Fox (Ed.), Wiley, New York, (1972), 19\u201346."}],"container-title":["Lecture Notes in Computer Science","Logics of Programs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0025790.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T16:55:30Z","timestamp":1607532930000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0025790"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354011212X"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/bfb0025790","relation":{},"subject":[]}}