[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
article
Free access

A critique of the foundations of Hoare style programming logics

Published: 01 December 1982 Publication History

Abstract

Much recent discussion in computing journals has been devoted to arguments about the feasibility and usefulness of formal verification methods. Too little attention has been given to precise criticism of specific proposed systems for reasoning about programs. Whether such systems are to be used for formal verification, by hand or automatically, or as a rigorous foundation for informal reasoning, it is essential that they be logically sound. Several popular rules in the Hoare language are, in fact, not sound. These rules have been accepted because they have not been subjected to sufficiently strong standards of correctness. This paper attempts to clarify the different technical definitions of correctness of a logic, to show that only the strongest of these definitions is acceptable for Hoare logic, and to correct some of the unsound rules that have appeared in the literature. The corrected rules are given merely to show that it is possible to do so. Convenient and elegant rules for reasoning about certain programming constructs will probably require a more flexible notation than Hoare's.

References

[1]
Alagic, S. and Arbib, M.A. The Design of Well-Structured and Correct Programs. Springer-Verlag, New York, (1978).
[2]
Apt, K.R. A sound and complete Hoare-like system for a fragment of Pascal. Report IW/78, Mathematisch Centrum, Afdeling Informatica, Amsterdam, (1978).
[3]
Arbib, M.A. and Alagi6, S. Proof rules for gotos. A cta lnformatica 11, 2, (1979), 139-148.
[4]
Ashcroft, E.A., Clint, M., and Hoare, C.A.R. Remarks on program proving: jumps and functions, Acta Informatiea 6, 3, (1976), 317.
[5]
Clarke, E.M. Programming language constructs for which it is impossible to obtain good Hoare-like axiom systems, JA CM 26, 1, (Jan. 1979), 129-147.
[6]
Clint, M. and Hoare, C.A.R. Program proving: jumps and functions A cta Informatica 1, 3 (1972), 214-224.
[7]
Constable, R. and O'Donnell, M. A Programming Logic. Winthrop, Cambridge Massachusetts, 1978.
[8]
Cook, S.A. Soundness and completeness of an axiom system for program verification. SIAM Journal on Computing 7, 1, (Feb. 1978), 70-90.
[9]
de Bakker, J.W., Klop, J.W., and Meyer, J.-J. Ch. Correctness of programs with function procedures. Preprint, Mathematisch Centrum, Amsterdam, (1981).
[10]
deBruin, A. Goto statements, semantics and deduction systems. (Preprint) Mathematisch Centrum, Amsterdam (1978).
[11]
de Bruin, A. Goto statements. In Chapter 10 of Mathematical Theory of Program Correctness by J. de Bakker. Prentice/Hall International, Englewood Cliffs, N J, (1980).
[12]
Dijkstra, E.W. Guarded commands, nondeterminacy and formal derivation of programs. Comm ACM 18, 8, (Aug. 1975), 453-457.
[13]
Donahue, J.E. Complementary Definitions of Programming Language Semantics. Lecture notes in Computer Science 42, Springer-Verlag, New York, (1976).
[14]
Floyd, R.W. Assigning meanings to programs. Proceedings of symposia in applied mathematics, 19, American Mathematical Society, Providence, (1967).
[15]
Hoare, C.A.R. An axiomatic basis for computer programming. Comm. ACM 12, 10, (Oct. 1969), 576-580.
[16]
Hoare, C.A.R. and Wirth, N. An axiomatic definition of the programming language PASCAL. Acta lnformatica 2, 4, (1973), 335- 355.
[17]
Kowaltowski, T. Axiomatic approach to side effects and general jumps. Acta Informatica 7, 4, (1977), 357-360.
[18]
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 lnformatica 10, 1, (1978), 1-26.
[19]
Manna, Z. and Waldinger, R. Is "sometime" sometimes better than "always"? Second International Conference on Software Engineering, San Francisco, (1976) pp. 32-39.
[20]
Mendelson, E. Introduction to Mathematical Logic. 2nd Ed., Van Nostrand, New York, (1976).
[21]
Musser, D. A proof rule for functions. USC Information Sciences Institute Tec. Rept. ISI/RR-77-62, (1977).
[22]
Olderog, E. Sound and complete Hoare-like calculi based on copy rules. Technical Report 7905, Christian-Albrechts Universit/it, Kiel, West Germany, (1979).
[23]
Russell, B. Letter to G. Frege, June 16, 1902. From Frege to Godel: A Source Book in Mathematical Logic, 1879-1931. J. van Heijenoort (Ed.), Harvard University Press, Cambridge, (1967), 124- 125.
[24]
Scott, D. and Strachey, C. Towards a mathematical semantics for computer languages. Computers and Automata. J. Fox (Ed.), Wiley, New York, (1972), 19-46.

Cited By

View all

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Communications of the ACM
Communications of the ACM  Volume 25, Issue 12
Dec 1982
84 pages
ISSN:0001-0782
EISSN:1557-7317
DOI:10.1145/358728
Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 December 1982
Published in CACM Volume 25, Issue 12

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Goto
  2. defined functions
  3. logic
  4. partial correctness
  5. proofs
  6. soundness

Qualifiers

  • Article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)103
  • Downloads (Last 6 weeks)7
Reflects downloads up to 25 Dec 2024

Other Metrics

Citations

Cited By

View all
  • (2023)Weakest preconditioned goto axiomInformation Processing Letters10.1016/j.ipl.2022.106329180:COnline publication date: 1-Feb-2023
  • (2021)Behind Clint and Hoare’s goto Proof Rule2021 International Symposium on Theoretical Aspects of Software Engineering (TASE)10.1109/TASE52547.2021.00021(23-30)Online publication date: Aug-2021
  • (2020)Hoare-Style Logic for Unstructured ProgramsSoftware Engineering and Formal Methods10.1007/978-3-030-58768-0_11(193-213)Online publication date: 14-Sep-2020
  • (2018)Formal Systems, Logics, and ProgramsRaymond Smullyan on Self Reference10.1007/978-3-319-68732-2_2(23-38)Online publication date: 14-Jan-2018
  • (2012)Deriving a Floyd–Hoare logic for non-local jumps from a formulæ-as-types notion of controlThe Journal of Logic and Algebraic Programming10.1016/j.jlap.2012.01.00481:3(181-208)Online publication date: Apr-2012
  • (2010)Semantic foundations for typed assembly languagesACM Transactions on Programming Languages and Systems10.1145/1709093.170909432:3(1-67)Online publication date: 16-Mar-2010
  • (2008)Hoare type theory, polymorphism and separation1Journal of Functional Programming10.1017/S095679680800695318:5-6(865-911)Online publication date: 1-Sep-2008
  • (2007)A compositional natural semantics and Hoare logic for low-level languagesTheoretical Computer Science10.1016/j.tcs.2006.12.020373:3(273-302)Online publication date: 30-Mar-2007
  • (2006)A Compositional Natural Semantics and Hoare Logic for Low-Level LanguagesElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2005.09.031156:1(151-168)Online publication date: 1-May-2006
  • (2006)A compositional logic for control flowProceedings of the 7th international conference on Verification, Model Checking, and Abstract Interpretation10.1007/11609773_6(80-94)Online publication date: 8-Jan-2006
  • Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Full Access

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media