# Computer Programs can be Proved Correct

Conference paper

## 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.

### References

- 1.Abrahams, P.W., Machine verification of mathematical proof. Sc. D. thesis, Massachusetts Institute of Technology, 1963Google Scholar
- 2.Burstall, R.M., Proving properties of programs by structural induction. Computer Journal, (to appear) 1969Google Scholar
- 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.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.Evans, A. Jr., Syntax analysis by a production language. Ph.D. thesis, Carnegie-Mellon University, 1965Google Scholar
- 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.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.Iverson, K.E., A Programming Language. John Wiley and Sons, New York, 1962MATHGoogle Scholar
- 9.Kaplan, P.M., Correctness of a compiler for Algol-like programs. Artificial Intelligence Memo. No. 48, Stanford University, 1967Google Scholar
- 10.Knuth, D.E., The Art of Computer Programming, Vol. 1 - Fundamental Algorithms. Addison-Wesley, Reading, Mass., 1968, section 1.2.1MATHGoogle Scholar
- 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.London, R.L., Correctness of the Algol procedure ASKFQRHAND. Computer Sciences Technical Report No. 50, University of Wisconsin, 1968Google Scholar
- 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.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.Moore, R.E., Interval Analysis. Prentice-Hall, Englewood Cliffs, N.J., 1966MATHGoogle Scholar
- 16.Naur P Proof of algorithms by general snapshots. BIT, Vol. 6, No. 4, 1966, pp. 310–316Google Scholar
- 17.Painter, J.A., Semantic correctness of a compiler for an Algol-like language. Artificial Intelligence Memo No. 44, Stanford University, 1967Google Scholar
- 18.Tobey, R.G., Rational function integration. Ph.D. thesis, Harvard University, 1967Google Scholar
- 19.Tobey, R.G., Personal communication. 1968Google Scholar
- 20.Wasserman, A.I., Bridge bidding by computer. Unpublished research, University of Wisconsin, undatedGoogle Scholar
- 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