Equivalence of the Gries and Martin proof rules for procedure calls.

Abstract

In this note we prove the equivalence of the proof rules for procedure calls as given by D. Gries [1] and A.J. Martin [2]. We also discuss a modification of these proof rules for the case that the specification of a procedure contains free constants.