Equivalence of the Gries and Martin proof rules for procedure calls
In this note the authors prove the equivalence of the proof rules for procedure calls as given by \textit{D. Gries} [The science of programming (Berlin 1981; Zbl 0472.68003)] and \textit{A. J. Martin} [Acta Inf. 20, 301- 313 (1983; Zbl 0546.68012)]. They also discuss a modification of these proof rules for the case that the specification of a procedure contains free constants.
scientific article; zbMATH DE number 3924104