Verification of Simple Recursive Programs in Theorema: Sufficient Conditions

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. We develop a method for proving total correctness properties of programs which have simple functional recursive definitions, and we discuss its different aspects. Most of the verification conditions are expressed in first order logic and their proof does not need a theory of computation, but only the knowledge which is specific to the functions occuring in the program.