Formal Aspects of Computing (1993) 5:554-570 @ 1993 BCS Formal Aspects of Computing Proof Rules for Recursive Procedures

Abstract. Four proof rules for recursive procedures in a Pascal-like language are presented. The main rule deals with total correctness and is based on results of Gries and Martin. The rule is easier to apply than Martin's. It is introduced as an extension of a specification format for Pascal-procedures, with its associated correctness and invocation rules. It uses well-founded recursion and is proved under the postulate that a procedure is semantically equal to its body. This rule for total correctness i compared with Hoare's rule for partial correct-ness of recursive procedures, in which no well-founded relation is needed. Both rules serve to prove correctness, i.e. sufficiency of certain preconditions. There are also two rules for proving necessity of preconditions. These rules can be used to give formal proofs of nontermination a d refinement. They seem to be completely new. 1. Announcement of Aims and Results In iterative programming, the proof rules for correctness are well established and have led to powerful methods for program derivation, culminating in [Kal90]. For recursive procedures in a language like Pascal, however, a generally accepted proof rule is still lacking. In [Hoa71], Hoare presented a derivation system to prove partial correctness of recursive procedures. This system has the disadvantages that it can only yield partial correctness and that it is incompatible with the full power of predicate calculus. In [Heh79] and [Mar83], methods are given to treat total correctness, but a concrete proof rule is not given. In particular, the combination of recursion and parameters emains implicit. The purpose of the present paper is to propose aproof rule for total correctnes