Is sometimes ever better than always?
The "intermittent assertion" method for proving programs correct is explained and compared to the conventional axiomatic method. Simple axiomatic proofs of iterative algorithms that compute recursively defined functions, including Ackermann's function, are given. A critical examination of the two methods leads to the opinion that the axiomatic method is preferable.
KeywordsIterative Algorithm Axiomatic Approach Control Return Total Correctness Loop Body
Unable to display preview. Download preview PDF.
- Manna, Z. and R. Waldinger. Is "sometime" sometimes better than "always"? CACM 21 (February 1978), 159–171.Google Scholar
- Hoare, C.A.R. An axiomatic basis for computer programming. CACM 12 (October 1969), 576–580, 583.Google Scholar
- Dijkstra, E.W. A Discipline of Programming, Prentice Hall, 1976.Google Scholar
- Knuth, D.E. The Art of Computer Programming, Vol. I, Addison-Wesley, Reading, Mass. 1968.Google Scholar
- Burstall, R.M. Program proving as hand simulation with a little induction. Proc. IFIP Congress 1974, Amsterdam. (308–312).Google Scholar
- Topor, R.W. A simple proof of the Schorr-Waite garbage collection algorithm, to appear in Acta Informatica?Google Scholar
- Gries, D. The Schorr-Waite graph marking algorithm. Computer Science, Cornell University, 1977. Submitted to Acta Informatica.Google Scholar
- Gries, D. An exercise in proving parallel programs correct. CACM 20 (December 1977), 921–930.Google Scholar
- Soundararajan, N. Axiomatic proofs of total correctness of programs. NCSDCT, Tata Inst. of Fundamental Research, Bombay, India, 1978.Google Scholar