Jim Woodcock and Ana Cavalcanti and Augusto Sampaio February 1997, Revised in June 1997 1pp.
Morgan and Back have proposed different formalisations of procedures and parameters in the context of techniques of program development based on refinement. We investigate a surprising and intricate relationship between these works and the substitution operator that renames the free variables of a program, and reveal an inconsistency in Morgan's refinement calculus. Back's formalisation of procedures does not suffer from this inconsistency, but his work is not as appealing to practising programmers as Morgan's calculus, whose distinctive feature is a large number of refinement laws. Here we benefit from both works and use Back's formalism as a model to derive the laws presented in Morgan's calculus. Keywords: program development, formal methods, refinement calculus, procedures, parameters.