A critique of the foundations of Hoare style programming logics

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: Suad Alagic , Michael A. Arbib, Design of Well-Structured and Correct Programs, Springer-Verlag New York, Inc., Secaucus, NJ, 1991
• 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: Edmund Melson Clarke, Jr., Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems, Journal of the ACM (JACM), v.26 n.1, p.129-147, Jan. 1979 [doi>10.1145/322108.322121]
• 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: Edsger W. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, v.18 n.8, p.453-457, Aug. 1975 [doi>10.1145/360933.360975]
• 13: James Edward Donahue, Complementary Definitions of Programming Language Semantics, Springer-Verlag New York, Inc., Secaucus, NJ, 1976
• 14: Floyd, R.W. Assigning meanings to programs. Proceedings of symposia in applied mathematics, 19, American Mathematical Society, Providence, (1967).
• 15: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 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: Zohar Manna , Richard Waldinger, Is “sometime” sometimes better than “always”?: Intermittent assertions in proving program correctness, Proceedings of the 2nd international conference on Software engineering, p.32-39, October 13-15, 1976, San Francisco, California, United States
• 20: Elliott Mendelson, Introduction to mathematical logic (3rd ed.), Wadsworth Publ. Co., Belmont, CA, 1987
• 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.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

General Terms:
Verification

Keywords:
Goto, defined functions, logic, partial correctness, proofs, soundness