A Practical Approach to Proving Termination of Recursive Programs in Theorema
Nikolaj Popov, Tudor Jebelean · 2004
Abstract. We report work in progress concerning the theoretical basis and the implementation in the Theorema system of a methodology for the generation of verification conditions for recursive procedures, with the aim of practical verification of recursive programs. Proving total correctness is achieved by proving separately partial correctness and then termination. In contrast to other approaches, which use a special theory describing the behavior of programs, we use such a theory only “in the background”, for developing a general rule for generating verification conditions, while the conditions themselves are presented (and provable) using the theories relevant to the program text only. This is very important for automatic proving, since it reduces significantly the effort of the provers. We performed practical experiments in which various programs are completely verified using the verification condition generator and the provers of the Theorema system. Introduction. While proving [partial] correctness of non-recursive procedural programs is quite well understood, for instance by using Hoare Logic [3], [6], there are relatively few approaches to recursive procedures (see e.g. [8] Chap. 2). We discuss here a practical approach to automatic generation of verification conditions for functional recursive programs, partially based on Scott induction in the fixpoint theory