Auxiliary variables and recursive procedures

Abstract

Much research in axiomatic semantics suffers from a lack of formality~ In particular, most proposed verification calculi for imperative programs dealing with recursive procedures are known to be unsound or incomplete. Focussing on total correctness, we present a new consequence rule which yields a sound and complete Hoare-style calculus in the presence of parameterless recursive procedures. Both, the standard consequence and an improved rule of adaptation are instances of our new rule. This work has been developed under the auspices of the computer-aided proof system LEGO. The rigorous treatment of auxiliary variables has been crucial for establishing our results. A comparison with VDM reinforces our view that auxiliary variables deserve to be treated seriously.