We present a (the first?)sou nd and relatively complete Hoare logic for a simple imperative programming language including mutually recursive procedures with call-by-value parameters as well as global and local variables. For such a language we formalize an operational and an axiomatic semantics of partial correctness and prove their equivalence. Global and local variables, including parameters, are handled in a rather straightforward way allowing for both dynamic and simple static scoping. For the completeness proof we employ the powerful MGF (Most General Formula)a pproach, introducing and comparing three variants for dealing with complications arising from mutual recursion.