  We provide a sound and relatively complete Hoare-like proof system for
reasoning about partial correctness of recursive procedures in presence of
local variables and the call-by-value parameter mechanism, and in which the
correctness proofs are linear in the length of the program. We argue that in
spite of the fact that Hoare-like proof systems for recursive procedures were
intensively studied, no such proof system has been proposed in the literature.
