Summary
This paper presents a uniform approach to known and new results on relative completeness of Hoare-like calculi for languages of ALGOL-like programs with procedures as procedure parameters. First the notion of a copy rule is introduced. It provides a uniform framework for dealing with different variants of semantics reaching from dynamic to static scope. Then for each copy rule ℒ a Hoare-like calculus ℋ(ℒ) is presented, the soundness of which is shown by using an approximating semantics. The key to the completeness results lies in a general completeness theorem on the calculi ℋ(ℒ) which has these results as corollaries. Finally, a new type of theorem on Hoare-like calculi is proved by which the notion of formal provability in ℋ(ℒ) is completely characterized. This characterization theorem is the main result of the paper. It covers both soundness and completeness of the calculi ℋ(ℒ) and additionally gives an idea of what the limits of presently known Hoare-like proof techniques for programming languages with procedures are.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Apt, K.R.: A sound and complete Hoare-like system for a fragment of PASCAL. Report IW 96/78. Mathematisch Centrum, 1978
Apt, K.R.: Ten years of Hoare's logic, a survey, part I. Tech. Report, Faculty of Economics, Erasmus Univ., Rotterdam, April 1979 ACM TOPLAS (in press, 1981)
Apt, K.R., de Bakker, J.W.: Semantics and proof theory of PASCAL procedures. In: Proc. 4th Coll. Automata, Languages and Programming (A. Salomaa, M. Steinby, eds.). Lecture Notes in Computer Science Vol. 52, pp. 30–44. Berlin-Heidelberg-New York: Springer 1977
Backus, J.W., Bauer, F.L., Green, J., Katz, C., McCarthy, J., Naur, P., Perlis, A.J., Rutishauser, H., Samelson, K., Vauquois, B., Wegstein, J.H., van Wijngaarden, A., Woodger, M.: Revised report on the algorithmic language ALGOL 60 (P. Naur, ed.) Numer. Math. 4, 420–453 (1963)
de Bakker, J.W.: Semantics and the foundation of program proving. In: Proc. IFIP Congress 1977, Toronto, pp. 279–284. Amsterdam: North Holland 1977
de Bakker, J.W.: Mathematical theory of programm correctness. London: Prentice Hall International 1980
Bergstra, J.A., Tucker, J.V.: Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs. Theor. Comput. Sci. (in press, 1981)
Cartwright, R., Oppen, D.: Unrestricted procedure calls in Hoare's logic. In: Proc. of the Fith Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, pp. 131–140. New York: ACM 1978
Clarke, E.M.: Programming language constructs for which it is impossible to obtain good Hoarelike axioms. J. Assoc. Comput. Mach. 26, 129–147 (1979)
Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7, 70–90 (1978)
Dijkstra, E.W.: Recursive programming. Numer. Math. 2, 312–318 (1960)
Donahue, J.E.: Complementary definitions of programming language semantics. Lecture Notes in Computer Science Vol. 42. Berlin-Heidelberg-New York: Springer 1976
Gorelick, G.A.: A complete axiomatic system for proving assertions about recursive and nonrecursive programs. Tech. Rep. 75, Dept. of Computer Sci., Univ. of Toronto (1975)
Grau, A.A., Hill, U., Langmaack, H.: Translation of ALGOL 60. Handbook for Automatic Computation, Vol. I, Part b. (Grundlehren der mathematischen Wissenschaften, Band 137) (K. Samelson, ed.) Berlin-Heidelberg-New York: Springer 1967
Gries, D., Levin, G.: Assignment and procedure call proof rules. ACM TOPLAS 2, 564–579 (1980)
Guttag, J.V., Horning, J.J., London, R.L.: A proof rule for EUCLID procedures. In: Formal description of Programming Concepts (E.J. Neuhold, ed.), pp. 211–220. Amsterdam: North Holland 1978
Harel, D., Pnueli, A., Stavi, J.: A complete axiomatic system for proving deductions about recursive programs. In: Proc. of the 9th ACM Symposium on Theory of Computing, pp. 249–260. New York: ACM 1977
Hoare, C.A.R.: An axiomatic basis for computer programming. Comm. ACM 12, 576–580, 583 (1969)
Hoare, C.A.R.: Procedures and parameters: An axiomatic approach. In: Symposium on semantics of algorithmic languages (E. Engeler, ed.). Lecture Notes in Mathematics 188, pp. 102–116. Berlin-Heidelberg-New York: Springer 1971
Igarashi, S., London, R.L., Luckham, D.C.: Automatic program verfication I: A logical basis and its implementation. Acta Informat. 4, 145–182 (1975)
Jensen, K., Wirth, N: PASCAL user manual and report. Berlin-Heidelberg-New York: Springer 1975
Kandzia, P.: On the “most recent” property of ALGOL-like programs. In: Proc. 2nd Coll. Automata, Languages and Programming (J. Loeckx, ed.). Lecture Notes in Computer Science Vol. 14, pp. 97–111. Berlin-Heidelberg-New York: Springer 1974
Kandzia, P., Langmaack, H.: On a theorem of McGowan concerning the “most recent” property of programs. Bericht Nr. A 74/07 des Fachbereichs Angew. Math. und Inform., Univ. d. Saarlandes (1974)
Klein, H.-J.: Untersuchungen im Zusammenhang mit der “most recent” Eigenschaft von Pro-Programmen. Bericht Nr. 8/77 des Inst. f. Inform. u. Prakt. Math., Christian-Albrechts-Univ., Kiel 1977
Klein, H.-J.: Zur Charakterisierung von Programmen mit endlichen Arten. Dissertation, Christian-Albrechts-Univ., Kiel 1980
Langmaack, H.: On correct procedure parameter transmission in higher programming languages. Acta Informat. 2, 110–142 (1973)
Langmaack, H.: On procedures as open subroutines I, II. Acta Informat. 2, 311–333 (1973) and Acta Informat. 3, 227–241 (1974)
Langmaack, H.: On a theory of decision problems in programming languages. In: Proc. of the Int. Conf. on Math. Studies of Inform. Processing, Kyoto (E.K. Blum, S. Takasu, eds.). Lecture Notes in Computer Science Vol. 75, pp. 538–558. Berlin-Heidelberg-New York: Springer 1969
Langmaack, H.: On termination problems for finitely interpreted ALGOL-like programs. Bericht Nr. 7904 des Inst. f. Inform, u. Prakt. Math., Christian-Albrechts-Univ., Kiel, 1979
Langmaack, H.: A proof of a theorem of Lipton on Hoare logic and applications. Bericht Nr. 8003 des Inst. f. Inform, u. Prakt. Math., Christian-Albrechts-Univ., Kiel, 1980
Langmaack, H., Olderog, E.-R.: Present-day Hoare-like systems for programming languages with procedures: power, limits and most likely extensions. In: Proc. 7th Coll. Automata, Languages and Programming (J.W. de Bakker, J. van Leeuwen, eds.). Lecture Notes in Computer Science Vol. 85, pp. 363–373. Berlin-Heidelberg-New York: Springer 1980
Lauer, P.E.: Consistent formal theories of the semantics of programming languages. Tech. Rep. TR 25.121, IBM Laboratory, Vienna 1971
Lipton, R.J.: A necessary and sufficient condition for the existence of Hoare logics. In: 18th IEEE Symposium on Foundations of Computer Science, Providence, Rhode Island, pp. 1–6. New York: IEEE 1977
London, R.L., Guttag, J.V., Horning, J.J., Lampson, B.W., Mitchell, J.G., Popek, G.J.: Proof rules for the programming language EUCLID. Acta Informat. 10, 1–26 (1978)
McGowan, C.L.: The “most recent” error: its causes and correction. SIGPLAN Notices 7, 191–202 (1972)
O'Donnell, M.J.: A critique of the foundations of Hoare-style programming logic. Tech. Report, Computer Sci. Dept., Purdue Univ., West-Lafayette, 1980
Olderog, E.-R.: Korrektheits- und Vollständigkeitsaussagen über Hoaresche Ableitungskalküle. Diplomarbeit, Christian-Albrechts-Univ., Kiel 1979
Prawitz, D.: Natural deduction — a proof-theoretic study. Stockholm: Almqvist and Wiksell 1965
Randell, B., Russell, L.J.: ALGOL 60 implementation. London: Academic Press, 1964
Schwartz, R.L.: An axiomatic definition of ALGOL 68. Comp. Sci. Dept., UCLA-34P214-75, Univ. of California, Los Angeles, 1978
Schwartz, R.L.: On axiomatizability as a language design tool. Dept. of Applied Maths., Weizmann Inst. of Sci., Rehovot, January 1979
Schwarz, J.: Generic commands — a tool for partial correctness formalism. Comput. J. 20, 151–155 (1977)
Sieber, K.: A new Hoare-calculus for programs with recursive parameterless procedures. Bericht A 81/02 des Fachbereichs Angew. Math. u. Inform., Univ. d. Saarlandes, Saarbrücken 1981
Wand, M.: A new incompleteness result for Hoare's system. J. Assoc. Comput. Mach. 25, 168–175 (1978)
van Wijngaarden, A., Mailloux, B.J., Peck, J.E.L., Koster, C.H.A., Sintzoff, M., Lindsey, C.H., Meertens, L.G.L.T., Fisker, R.G. (eds.): Revised report on the algorithmic language ALGOL 68. Acta Informat. 5, 1–236 (1975)
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Olderog, ER. Sound and complete Hoare-like calculi based on copy rules. Acta Informatica 16, 161–197 (1981). https://doi.org/10.1007/BF00261258
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF00261258