An inconsistency in procedures, parameters, and substitution in the refinement calculus

Morgan and Back have proposed different formalisations of procedures and parameters in the context of techniques of program development based on refinement. In this paper, we investigate a surprising and intricate relationship between these works and the substitution operator that renames the free variables of a program. In this study, we reveal an inconsistency in Morganʹs refinement calculus and show that Backʹs formalisation of procedures does not have the same problem.