A complete axiomatic system for proving deductions about recursive programs
David Harel, Amir Puneli, Jonathan Stavi · 1977
Denoting a version of Hoare's system for proving partial correctness of recursive programs by H, we present an extension D which may be thought of as H υ {@@@@,@@@@,@@@@,@@@@} υ H-1, including the rules of H, four special purpose rules and inverse rules to those of Hoare. D is shown to be a complete system (in Cook's sense) for proving deductions of the form σ1,....σn @@@@ σ over a language, the wff's of which are assertions in some assertion language L and partial correctness specifications of the form p(α)q. All valid formulae of L are taken as axioms of D. It is shown that D is sufficient for proving partial correctness, total correctness and program equivalence as well as other important properties of programs, the proofs of which are impossible in H. The entire presentation is worked out in the framework of nondeterministic programs employing iteration and mutually recursive procedures.