Is sometimes ever better than always?

  • David Gries
II. Program Verification
Part of the Lecture Notes in Computer Science book series (LNCS, volume 69)


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.


Iterative Algorithm Axiomatic Approach Control Return Total Correctness Loop Body 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Manna, Z. and R. Waldinger. Is "sometime" sometimes better than "always"? CACM 21 (February 1978), 159–171.Google Scholar
  2. [2]
    Hoare, C.A.R. An axiomatic basis for computer programming. CACM 12 (October 1969), 576–580, 583.Google Scholar
  3. [3]
    Dijkstra, E.W. A Discipline of Programming, Prentice Hall, 1976.Google Scholar
  4. [4]
    Knuth, D.E. The Art of Computer Programming, Vol. I, Addison-Wesley, Reading, Mass. 1968.Google Scholar
  5. [5]
    Burstall, R.M. Program proving as hand simulation with a little induction. Proc. IFIP Congress 1974, Amsterdam. (308–312).Google Scholar
  6. [6]
    Topor, R.W. A simple proof of the Schorr-Waite garbage collection algorithm, to appear in Acta Informatica?Google Scholar
  7. [7]
    Gries, D. The Schorr-Waite graph marking algorithm. Computer Science, Cornell University, 1977. Submitted to Acta Informatica.Google Scholar
  8. [8]
    Gries, D. An exercise in proving parallel programs correct. CACM 20 (December 1977), 921–930.Google Scholar
  9. [9]
    Soundararajan, N. Axiomatic proofs of total correctness of programs. NCSDCT, Tata Inst. of Fundamental Research, Bombay, India, 1978.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1979

Authors and Affiliations

  • David Gries
    • 1
  1. 1.Department of Computer ScienceCornell UniversityIthaca

Personalised recommendations