Termination assertions for recursive programs: Completeness and axiomatic definability

The termination assertion p〈S〉 q means that whenever the formula p is true, there is an execution of the possibly nondeterministic program S which terminates in a state in which q is true. The program S may declare and use local variables and nondeterministic procedures with call-by-value and call-by-address parameters. In addition, the program may call undeclared global procedures. Formulas p and q are first-order formulas extended to express hypotheses about the termination of calls to undeclared procedures. A complete effective axiom system with rules corresponding to the syntax of the programming language is given for the termination assertions valid over all interpretations. Termination assertions define the semantics of programs in the following sense: if two programs have different input-output semantics, then there is a temination assertion that is valid for one program but not the other. Thus the complete axiomatization of termination assertions is an axiomatic definition of the semantics of recursive programs