Abstract
We consider the problem of designing arithmetically complete axiom systems for proving general properties of programs; i.e. axiom systems which are complete over arithmetical universes, when all first-order formulae which are valid in such universes are taken as axioms. We prove a general Theorem of Completeness which takes care of a major part of the responsibility when designing such systems. It is then shown that what is left to do in order to establish an arithmetical completeness result, such as those appearing in [12] and [14] for the logics DL and DL+, can be described as a chain of reasoning which involves some simple utilizations of arithmetical induction. An immediate application of these observations is given in the form of an arithmetical completeness result for a new logic similar to that of Salwicki [22]. Finally, we contrast this discipline with Cook's [5] notion of relative completeness.
This report was prepared with the support of the National Science Foundation under NSF grant no. MCS76-18461.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
9. References
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–357. 1975.
deBakker, J.W. and W.P. deRoever. A Calculus for Recursive Program Schemes. in Automata, Languages and Programming (ed. Nivat), 167–196. North Holland. 1972.
Banachowski, L. Modular Properties of Programs. Bull. Acad. Pol. Sci., Ser. Sci. Math. Astr. Phys. Vol. 23. No. 3. 1975.
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–20. Jan. 1977.
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.)
Dijkstra, E.W. Cuarded Commands, Nondeterminacy and Formal Derivation of Programs. CACM Vol. 18, no. 8. 1975
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–32. 1967.
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.
Harel, D. Logics of Programs: Axiomatics and Descriptive Power. Ph.D. Thesis. Dept. of EECS. MIT, Cambridge MA. June. 1978.
Harel, D. Complete Axiomatization of Properties of Recursive Programs. Submitted for publication.
Harel, D. On the Correctness of Regular Deterministic Programs; A Unified Survey. Submitted for publication.
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–268, Boulder, Col., May 1977.
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.
Harel, D. and V.R. Pratt. Nondeterminism in Logics of Programs. Proc. 5th ACM Symp. on Principles of Programming Languages. Tucson, Ariz. Jan. 1978.
Hoare, C.A.R. An Axiomatic Basis for Computer Programming. CACM 12, 576–580. 1969.
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.
Lipton, R.J. and L. Snyder. Completeness and Incompleteness of Hoare-like Axiom Systems. Manuscript. Dept. of Computer Science. Yale University, 1977.
Manna, Z. The Correctness of Programs. JCSS 3. 119–127. 1969.
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.
Naur, P. Proof of Algorithms by General Snapshots. BIT 6. 310–316. 1966.
Pratt, V.R. Semantical Considerations on Floyd-Hoare Logic. 17th IEEE Symposium on Foundations of Computer Science, 109–121, Oct. 1976.
Salwicki, A. Formalized Algorithmic Languages. Bull. Acad. Pol. Sci., Ser. Sci. Math. Astr. Phys. Vol. 18. No. 5. 1970.
Wand, M. A New Incompleteness Result for Hoare's System. Proc. 8th ACM Symp. on Theory of Computing, 87–91. Hershey, Penn. May 1976.
Winklmann, K. Equivalence of DL and DL+ for regular programs. Manuscript, Lab. for Computer Science. MIT, Cambridge, MA. March. 1978.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1978 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Harel, D. (1978). Arithmetical completeness in logics of programs. In: Ausiello, G., Böhm, C. (eds) Automata, Languages and Programming. ICALP 1978. Lecture Notes in Computer Science, vol 62. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-08860-1_20
Download citation
DOI: https://doi.org/10.1007/3-540-08860-1_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-08860-8
Online ISBN: 978-3-540-35807-7
eBook Packages: Springer Book Archive