Proving total correctness of recursive procedures (Q913478)

Research in formalisation of program correctness has come up with various programming logics, e.g. Hoare logic, dynamic logic and temporal logic. These logics have been conceived to prove partial/total correctness of programs. To achieve this goal a proof system, i.e. a set of axioms along with some deduction rules, is to set up to reason about total correctness. A proof system being a formal logic system is considered feasible, if it is both sound and complete. Soundness guarantees that the proof system really describes the program in question; completeness entails that only valid correctness formulas can be derived. There are several proof systems that fail to observe either soundness of completeness when applied to prove total correctness of recursive procedures. The authors point out that the rules for this proof interact with rules set up to formalise invariance properties of ordinary procedure calls. They develop a proof system to separate the interpretations of these two program constructs and show that both sound- and completeness emerge quite naturally. The methods are first applied to a Hoare-style proof system, but are in turn used to modify a proof system based on dynamic logic to yield the same results. Their proof systems give way to simpler rules for recursive procedures without artificial extension to the programming language examined.