Predicate Transformers for Recursive Procedures with Local Variables
Wim H. Hesselink · Formal Aspects of Computing · 1999
Abstract. 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.