Program verification: the very idea

ABSTRACT

The notion of program verification appears to trade upon an equivocation. Algorithms, as logical structures, are appropriate subjects for deductive verification. Programs, as causal models of those structures, are not. The success of program verification as a generally applicable and completely reliable method for guaranteeing program performance is not even a theoretical possibility.

REFERENCES

• 1: Benacerra~ P. and Putnam, H., Eds. Philosophy of Mathematics: Selected Readings. Prentice-Hall, Englewood Cliffs, N.J. 1964.
• 2: Black, M. Induction. The Encyclopedia of Philosophy, vol. 4, Edwards, P., Editor-in-Chief. Macmillan, New York, 1967, pp. 169-181.
• 3: Blumberg, A. Logic, modern, The Encyclopedia of Philosophy, vol. 5, Edwards, P., Editor-in-Ghie~ Macmillan, New York, 1967, pp. 12-34.
• 4: Bochner, S. The Role of Mathematics in the Rise of Science. Princeton Univ. Press, Princeton, N.J. 1966.
• 5: Cerutti, E. and Davis, P. Formac meets Pappus. Am. Math. Monthly 76 (1969), 895-904.
• 6: Church, A. Logistic system. Dictionary of Philosophy. Runes, D., Ed. Littlefield, Adams & Co., Ames, Iowa, 1959, pp. 182-183.
• 7: Dancy, J. An Introduction to Contemporary Epistemology. Blackwell, Oxford, 1985.
• 8: Richard A. De Millo , Richard J. Lipton , Alan J. Perlis, Social processes and proofs of theorems and programs, Communications of the ACM, v.22 n.5, p.271-280, May 1979 [doi>10.1145/359104.359106]
• 9: Detlefsen, M. and Luker, M. The four-color theorem and mathematical proof. J. Philos. 77, 12 (December 1980), 803-820.
• 10: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 11: Fetzer, J. H. Scientific Knowledge. Reidel, Dordrecht, Holland, 1981.
• 12: Fetzer, J. H. Signs and minds: An introduction to the theory of semiotic systems. In Aspects of Artificial Intelligence, Fetzer, J., Ed. Kluwer, Dordrecht/Boston/London/Tokyo, 1988, pp. 133-161.
• 13: Glazer, D. Letter to the editor. Commun. ACM 22, 11 (November 1979), 621.
• 14: Hacking, I. Slightly more realistic personal probabilities. Philos. Sci. 34, 4 (December 1967), 311-325.
• 15: Heise, D. R. Causal Analysis. Wiley, New York, 1975.
• 16: Hempel, C. G. On the nature of mathematical truth. In Readings in Philosophical Analysis, Feigl, H. and Sellars, W., Eds. Appleton- Century-Crofts, New York, 1949, pp. 222-237.
• 17: Hempel, C. G. Geometry and empirical science. In Readings in Philosophical Analysis, Feigl, H. and Sellars, W., Eds. Appleton-Century- Crofts, New York, 1949, pp. 238-249.
• 18: Hesse, M. Models and Analogies in Science. Univ. of Notre Dame Press, Notre Dame, Ind., 1966.
• 19: 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]
• 20: Hoare, C. A. R. Mathematics of programming. BYTE (August 1986), 115-149.
• 21: Holt, R. Design goals for the Turing programming language. Technical Report GSRI-187 (Aug. 1986), Computer Systems Research Institute, Univ. of Toronto.
• 22: R. Kling, Defining the boundaries of computing across complex organizations, Critical issues in information systems research, John Wiley & Sons, Inc., New York, NY, 1987
• 23: Kuhn, T. S. The Structure of Scientific Revolutions, 2d ed. Univ. of Chicago Press, Chicago, 1970.
• 24: Lakatos, I. Proofs and Refutations. Cambridge Univ. Press, Cambridge, U.K., 1976.
• 25: Lakatos, I., and Musgrave, A., Eds. Criticism and the Growth of Knowledge. Cambridge Univ. Press, Cambridge, U.K., 1970.
• 26: Lamport, L. Letter to the editor. Commun. ACM 22, 11 (November 1979), 624.
• 27: Michael Marcotty , Henry F. Ledgard, Programming language landscape: syntax, semantics, and implementation, SRA School Group, 1986
• 28: Maurer, W. D. Letter to the editor, Commun. ACM 22, 11 (November 1979), 625-629.
• 29: Michalos, A. Principles of Logic. Prentice-Hall, Englewood Cliffs, N.J., 1969.
• 30: Moor, J. H. The pseudorealization fallacy and the Chinese room. In Aspects of Artificial Intelligence. Fetzer, J. Ed. Kluwer, Dordrecht/ Boston/London/Tokyo, 1988, pp. 35-53.
• 31: Pagels, H. The Cosmic Code. Simon & Schuster, New York, 1982.
• 32: Popper, K. R. Conjectures and Refutations. Harper & Row, New York, 1965.
• 33: Popper, K. R. Objective Knowledge. Clarendon Press, Oxford, 1972.
• 34: Suppe, F., Ed. The Structure of Scientific Theories, 2d ed. University of Illinois Press, Urbana, Ill., 1977.
• 35: Teller, P. Computer proof. J. Philos. 77, 12 (December 1980), 797-803.
• 36: Tymoczko, T. The four-color theorem and its philosophical significance. J. Philos. 76, 2 (February 1979), 57-83.
• 37: van den Bos, J. Letter to the editor. Commun. ACM 22, 11 (November 1979), 623.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Validation

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Methodologies (e.g., object-oriented, structured)
      D.2.5 Testing and Debugging
          Subjects: Diagnostics

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.3 Complexity Measures and Classes
          Subjects: Relations among complexity classes
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Complexity of proof procedures

General Terms:
Algorithms, Experimentation, Human Factors, Performance, Reliability, Verification