{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T03:27:50Z","timestamp":1777519670874,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540088608","type":"print"},{"value":"9783540358077","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1978]]},"DOI":"10.1007\/3-540-08860-1_20","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T16:34:00Z","timestamp":1330187640000},"page":"268-288","source":"Crossref","is-referenced-by-count":10,"title":["Arithmetical completeness in logics of programs"],"prefix":"10.1007","author":[{"given":"David","family":"Harel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,26]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/S0022-0000(75)80056-0","volume":"11","author":"J. W. deBakker","year":"1975","unstructured":"deBakker, J.W. and L.G.L.T. Meertens. On the Completeness of the Inductive Assertion Method. J. of Computer and System Sciences, 11, 323\u2013357. 1975.","journal-title":"J. of Computer and System Sciences"},{"key":"20_CR2","unstructured":"deBakker, J.W. and W.P. deRoever. A Calculus for Recursive Program Schemes. in Automata, Languages and Programming (ed. Nivat), 167\u2013196. North Holland. 1972."},{"key":"20_CR3","unstructured":"Banachowski, L. Modular Properties of Programs. Bull. Acad. Pol. Sci., Ser. Sci. Math. Astr. Phys. Vol. 23. No. 3. 1975."},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Clarke, E.M. Programming Language Constructs for which it is impossible to obtain good Hoare-like Axiom Systems. Proc. 4th ACM Symp. on Principles of Programming Languages. 10\u201320. Jan. 1977.","DOI":"10.1145\/512950.512952"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Cook, S.A. Soundness and Completeness of an Axiom System for Program Verification, SIAM J. Comp. Vol. 7, no. 1. Feb. 1978. (A revision of: Axiomatic and Interpretive Semantics for an Algol Fragment, TR-79. Dept. of Comuter Science, U. of Toronto. 1975.)","DOI":"10.1137\/0207005"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W. Cuarded Commands, Nondeterminacy and Formal Derivation of Programs. CACM Vol. 18, no. 8. 1975","DOI":"10.1145\/360933.360975"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Floyd, R.W. Assigning Meaning to Programs. In J.T. Schwartz (ed.) Mathematical Aspects of Computer Science. Proc. Symp. in Applied Math. 19. Providence, R.I. American Math. Soc. 19\u201332. 1967.","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"20_CR8","unstructured":"Corelick, G.A. A Complete Axiomatic System for Proving Assertions about Recursive and Nonrecursive Programs. TR-75. Dept. of Computer Science, U. of Toronto. 1975."},{"key":"20_CR9","volume-title":"Logics of Programs: Axiomatics and Descriptive Power","author":"D. Harel","year":"1978","unstructured":"Harel, D. Logics of Programs: Axiomatics and Descriptive Power. Ph.D. Thesis. Dept. of EECS. MIT, Cambridge MA. June. 1978."},{"key":"20_CR10","unstructured":"Harel, D. Complete Axiomatization of Properties of Recursive Programs. Submitted for publication."},{"key":"20_CR11","unstructured":"Harel, D. On the Correctness of Regular Deterministic Programs; A Unified Survey. Submitted for publication."},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Harel, D., A.R. Meyer and V.R. Pratt. Computability and Completeness in Logics of Programs. Proc. 9th Ann. ACM Symp. on Theory of Computing, 261\u2013268, Boulder, Col., May 1977.","DOI":"10.1145\/800105.803416"},{"key":"20_CR13","unstructured":"Harel, D., A. Pnueli and J. Stavi. Completeness Issues for Inductive Assertions and Hoare's Method. Technical Report, Dept of Appl. Math. Tel-Aviv U. Israel. Aug. 1976."},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Harel, D. and V.R. Pratt. Nondeterminism in Logics of Programs. Proc. 5th ACM Symp. on Principles of Programming Languages. Tucson, Ariz. Jan. 1978.","DOI":"10.1145\/512760.512782"},{"key":"20_CR15","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. CACM 12, 576\u2013580. 1969.","journal-title":"CACM"},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"Lipton, R.J. A Necessary and Sufficient Condition for the Existence of Hoare Logics. 18th IEEE Symposium on Foundations of Computer Science, Providence, R.I. Oct. 1977.","DOI":"10.1109\/SFCS.1977.1"},{"key":"20_CR17","unstructured":"Lipton, R.J. and L. Snyder. Completeness and Incompleteness of Hoare-like Axiom Systems. Manuscript. Dept. of Computer Science. Yale University, 1977."},{"key":"20_CR18","first-page":"119","volume":"3","author":"Z. Manna","year":"1969","unstructured":"Manna, Z. The Correctness of Programs. JCSS 3. 119\u2013127. 1969.","journal-title":"JCSS"},{"key":"20_CR19","volume-title":"Equivalence of DL, DL+ and ADL for Regular Programs with Array Assignments","author":"A. R. Meyer","year":"1977","unstructured":"Meyer, A.R. Equivalence of DL, DL+ and ADL for Regular Programs with Array Assignments. Manuscript. Lab. for Computer Science. MIT, Cambridge MA. August 1977."},{"key":"20_CR20","doi-asserted-by":"crossref","first-page":"310","DOI":"10.1007\/BF01966091","volume":"6","author":"P. Naur","year":"1966","unstructured":"Naur, P. Proof of Algorithms by General Snapshots. BIT 6. 310\u2013316. 1966.","journal-title":"BIT"},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"Pratt, V.R. Semantical Considerations on Floyd-Hoare Logic. 17th IEEE Symposium on Foundations of Computer Science, 109\u2013121, Oct. 1976.","DOI":"10.1109\/SFCS.1976.27"},{"key":"20_CR22","unstructured":"Salwicki, A. Formalized Algorithmic Languages. Bull. Acad. Pol. Sci., Ser. Sci. Math. Astr. Phys. Vol. 18. No. 5. 1970."},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"Wand, M. A New Incompleteness Result for Hoare's System. Proc. 8th ACM Symp. on Theory of Computing, 87\u201391. Hershey, Penn. May 1976.","DOI":"10.1145\/800113.803635"},{"key":"20_CR24","volume-title":"Equivalence of DL and DL+ for regular programs","author":"K. Winklmann","year":"1978","unstructured":"Winklmann, K. Equivalence of DL and DL+ for regular programs. Manuscript, Lab. for Computer Science. MIT, Cambridge, MA. March. 1978."}],"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-08860-1_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:00:03Z","timestamp":1605643203000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-08860-1_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1978]]},"ISBN":["9783540088608","9783540358077"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-08860-1_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1978]]}}}