Unrestricted procedure calls in Hoare's logic
Robert Cartwright, Derek C. Oppen · 1978
This paper presents a new version of Hoare's logic including generalized procedure call and assignment rules which correctly handle aliased variables. Formal justifications are given for the new rules.