Computer Programs can be Proved Correct

  • Ralph L. London
Part of the Lecture Notes in Operations Research and Mathematical Systems book series (LNE, volume 28)

Abstract

There has been much recent interest in proving the semantic correctness of computer programs, that is, in showing that computer programs meet their specifications or have certain desirable properties. The work of Burstall (1969), Cooper (1967), Floyd (1967), McCarthy (1963), McCarthy and Painter (1967) and Naur (1966) can be cited to demonstrate this interest. Moreover, it is now recognized that a program or algorithm ought to be accompanied by a proof of correctness. Even though this proof is seldom given, at least the need for such proof is recognized.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abrahams, P.W., Machine verification of mathematical proof. Sc. D. thesis, Massachusetts Institute of Technology, 1963Google Scholar
  2. 2.
    Burstall, R.M., Proving properties of programs by structural induction. Computer Journal, (to appear) 1969Google Scholar
  3. 3.
    Burstall, R.M. and Landin, P.J., Programs and their proofs: an algebraic approach, in Machine Intelligence 4, Meltzer, B. and Michie, D. (eds.), Edinburgh University Press, (to appear) 1969Google Scholar
  4. 4.
    Cooper, D.C., Mathematical proofs about computer programs, in Machine Intelligence 1, Collins, N.L. and Michie, D. (eds.), American Elsevier, New York, 1967, pp. 17–28Google Scholar
  5. 5.
    Evans, A. Jr., Syntax analysis by a production language. Ph.D. thesis, Carnegie-Mellon University, 1965Google Scholar
  6. 6.
    Floyd, R.W., Assigning meanings to programs, in Proceedings of a Symposium in Applied Mathematics, Vol. 19 - Mathematical Aspects of Computer Science, Schwarcz, J.T. (ed.), American Mathematical Society, Providence, R.I., 1967, pp. 19–32Google Scholar
  7. 7.
    Good, D.I. and London, R.L., Interval arithmetic for the Burroughs B5500: Four Algol procedures and proofs of their correctness”! Computer Science Technical Report No. 26, University of Wisconsin, 1968Google Scholar
  8. 8.
    Iverson, K.E., A Programming Language. John Wiley and Sons, New York, 1962MATHGoogle Scholar
  9. 9.
    Kaplan, P.M., Correctness of a compiler for Algol-like programs. Artificial Intelligence Memo. No. 48, Stanford University, 1967Google Scholar
  10. 10.
    Knuth, D.E., The Art of Computer Programming, Vol. 1 - Fundamental Algorithms. Addison-Wesley, Reading, Mass., 1968, section 1.2.1MATHGoogle Scholar
  11. 11.
    London, R.L. and Wasserman, A.I., The anatomy of an Algol procedure. Computer Sciences Technical Report No. 5, University of Wisconsin, 1967Google Scholar
  12. 12.
    London, R.L., Correctness of the Algol procedure ASKFQRHAND. Computer Sciences Technical Report No. 50, University of Wisconsin, 1968Google Scholar
  13. 13.
    McCarthy, J., Towards a mathematical science of computation, in Information Processing 1962 - Proceedings of IFIP Congress 62, Poppelwell, CM. (ed.), North-Holland, Amsterdam, 1963, pp. 21–28Google Scholar
  14. 14.
    McCarthy, J. and Painter, J.A., Correctness of a compiler for arithmetic expressions, in Proceedings of a Symposium in Applied Mathematics, Vol. 19 - Mathematical Aspects of Computer Science, Schwarcz, J.T. (ed.), American Mathematical Society, Providence, Rhode Island, 1967, pp. 33–41Google Scholar
  15. 15.
    Moore, R.E., Interval Analysis. Prentice-Hall, Englewood Cliffs, N.J., 1966MATHGoogle Scholar
  16. 16.
    Naur P Proof of algorithms by general snapshots. BIT, Vol. 6, No. 4, 1966, pp. 310–316Google Scholar
  17. 17.
    Painter, J.A., Semantic correctness of a compiler for an Algol-like language. Artificial Intelligence Memo No. 44, Stanford University, 1967Google Scholar
  18. 18.
    Tobey, R.G., Rational function integration. Ph.D. thesis, Harvard University, 1967Google Scholar
  19. 19.
    Tobey, R.G., Personal communication. 1968Google Scholar
  20. 20.
    Wasserman, A.I., Bridge bidding by computer. Unpublished research, University of Wisconsin, undatedGoogle Scholar
  21. 21.
    Yohe, J.M., Computer programming for accuracy. Mathematics Research Center Technical Summary Report No. 866, University of Wisconsin, 1968Google Scholar

Copyright information

© Springer-Verlag Berlin · Heidelberg 1970

Authors and Affiliations

  • Ralph L. London
    • 1
  1. 1.Computer Sciences DepartmentUniversity of WisconsinMadisonUSA

Personalised recommendations