Predicate Transformers for Recursive Procedures with Local Variables

The weakest precondition semantics of recursive procedures with local variables are developed for an imperative language with demonic and angelic operators for unbounded nondeterminate choice. This does not require stacking of local variables. The formalism serves as a foundation for a proof rule for total correctness of (mutually) recursive procedures with local variables. This rule is illustrated by a simple example. Its soundness is proved for arbitrary well-founded variant functions.