The synthesis of loop predicates

ABSTRACT

Current methods for mechanical program verification require a complete predicate specification on each loop. Because this is tedious and error prone, producing a program with complete, correct predicates is reasonably difficult and would be facilitated by machine assistance. This paper discusses techniques for mechanically synthesizing loop predicates. Two classes of techniques are considered: (1) heuristic methods which derive loop predicates from boundary conditions and/or partially specified inductive assertions: (2) extraction methods which use input predicates and appropriate weak interpretations to obtain certain classes of loop predicates by an evaluation on the weak interpretation.

REFERENCES

• 1: John Cocke, Programming languages and their compilers: Preliminary notes, Courant Institute of Mathematical Sciences, New York University, 1969
• 2: Cooper, D.C. Programs for mechanical program verification. In Machine Intelligence 6, American Elsevier, New York, 1971, pp. 43-59.
• 3: Deutsch, L.P. An interactive program verifier. Ph.D. Th., Dep. Comput, Sci., U. of California, Berkeley, Calif., June 1973.
• 4: Elspas, B., Green, M.W., Levitt, K.N., and Waldinger, R. J. Research in interactive program-proving techniques. SRI, Menlo Park, Calif., May 1972.
• 5: Bernard Elspas , Karl N. Levitt , Richard J. Waldinger , Abraham Waksman, An Assessment of Techniques for Proving Program Correctness, ACM Computing Surveys (CSUR), v.4 n.2, p.97-147, June 1972 [doi>10.1145/356599.356602]
• 6: Floyd, R. J. Assigning meanings to programs. In Proc. of a Symposium in Applied Mathematics, Vat. 19, J.T. Schwartz (Ed.), AMS, 1967, pp. 19-32.
• 7: Hewitt, C. PLANNER: A language for proving theorems and manipulating models in a robot. Ph.D. Th., MIT, Dep. Math., Jan. 1971.
• 8: Katz, S.M., and Manna, Z. A heuristic approach to program verification. Proc. 3rd Internat. Joint Conf. on Artif. Intel., Aug. 1973, pp. 500-512.
• 9: James Cornelius King, A program verifier, 1970
• 10: Ralph L. London, The current state of proving programs correct, Proceedings of the ACM annual conference, p.39-46, August 01-01, 1972, Boston, Massachusetts, United States [doi>10.1145/800193.805820]
• 11: McDermott, D.V., and Sussman, G.J. The CONNIVER reference manual. Memo No. 259, MIT, A.I. Lab., May 1972.
• 12: Rulifson, J.F., Derksen, J.A., and Waldinger, R.J. QA4: A procedural calculus for intuitive reasoning. Tech. Note 73, SRI, Nov. 1972.
• 13: Wegbreit, B. Property extraction in well-founded property sets. Tech. Rep., Cent. for Res. in Comput. Tech. Harvard U., Cambridge, Mass., Feb., 1973.
• 14: Vegbreit, B. Heuristic methods for mechanically deriving inductive assertions. Proc. 3rd Internat. Joint Conf. on Artif. Intel., Aug. 1973, pp. 524-536.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Concurrent programming structures

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.8 Problem Solving, Control Methods, and Search
          Subjects: Heuristic methods

General Terms:
Algorithms, Design, Languages, Theory, Verification

Keywords:
inductive assertions, loop predicates, program verification, property extraction, synthesis of loop predicates, theorem proving, weak interpretations, well-founded sets