Is “sometime” sometimes better than “always”?: intermittent assertions in proving program correctness

ABSTRACT

This paper explores a technique for proving the correctness and termination of programs simultaneously. This approach, the intermittent-assertion method, involves documenting the program with assertions that must be true at some time when control passes through the corresponding point, but that need not be true every time. The method, introduced by Burstall, promises to provide a valuable complement to the more conventional methods. The intermittent-assertion method is presented with a number of examples of correctness and termination proofs. Some of these proofs are markedly simpler than their conventional counterparts. On the other hand, it is shown that a proof of correctness or termination by any of the conventional techniques can be rephrased directly as a proof using intermittent assertions. Finally, it is shown how the intermittent-assertion method can be applied to prove the validity of program transformations and the correctness of continuously operating programs.

REFERENCES

• 1: Ashcroft, E.A., and Wadge, W.W. Intermittent-assertion proofs in Lucid. Information Processing 77, North-Holland Pub. Co., Amsterdam, 1977, pp. 723-726.
• 2: Burstall, R.M. Program proving as hand simulation with a little induction. Information Processing 74, North-Holland Pub. Co., Amsterdam, 1974, pp. 308-312.
• 3: R. M. Burstall , John Darlington, A Transformation System for Developing Recursive Programs, Journal of the ACM (JACM), v.24 n.1, p.44-67, Jan. 1977 [doi>10.1145/321992.321996]
• 4: Floyd, R.W. Assigning meaning to programs. Proc. Symp. in Applied Math. Vol. 19, J.T. Schwartz, Ed., Amer. Math. Soc., Providence, R.I., 1967, pp. 19-32.
• 5: Francez, N., and Pnueli, A. A proof method for cyclic programs. To appear in Acta Informatica.
• 6: Susan L. Gerhart, Correctness-preserving program transformations, Proceedings of the 2nd ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.54-66, January 20-22, 1975, Palo Alto, California [doi>10.1145/512976.512983]
• 7: 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]
• 8: Katz, S.M., and Manna, Z. A closer look at termination. Acta Informatica 5 (Dec. 1975), 333-352.
• 9: Donald E. Knuth, The art of computer programming, volume 1 (3rd ed.): fundamental algorithms, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1997
• 10: Donald E. Knuth, Structured Programming with go to Statements, ACM Computing Surveys (CSUR), v.6 n.4, p.261-301, Dec. 1974 [doi>10.1145/356635.356640]
• 11: Ralph L. London, A view of program verification, Proceedings of the international conference on Reliable software, p.534-545, April 21-23, 1975, Los Angeles, California
• 12: Manna, Z. Mathematical theory of partial correctness. J. Comptr. Syst. Sci. 5, 3 (June 1971), 239-253.
• 13: Zohar Manna, Introduction to Mathematical Theory of Computation, McGraw-Hill, Inc., New York, NY, 1974
• 14: James H. Morris, Jr. , Ben Wegbreit, Subgoal induction, Communications of the ACM, v.20 n.4, p.209-222, April 1977 [doi>10.1145/359461.359466]
• 15: Pratt, V.R. Semantical considerations on Floyd-Hoare logic. Proc. 17th Symp. on Foundations of Comptr. Sci., Houston, Tex., Oct. 1976, pp. 109-121.
• 16: Schwarz, J. Event-based reasoning-a system for proving correct termination of programs. Proc. Third Int. Colloquium on Automata, Languages and Programming, Edinburgh, Scotland, July 1976, pp. 131-146.
• 17: Topor, R.W. A simple proof of the Schorr-Waite garbage collection algorithm. To appear in Acta Informatica.
• 18: Wang, A. An axiomatic basis for proving total correctness of goto-programs. BIT 16 (1976), 88-102.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE

General Terms:
Design, Performance, Reliability, Theory, Verification

Keywords:
continuously operating programs, correctness of programs, intermittent assertions, program transformation, program verification, termination of programs