  This paper presents a wp-style calculus for obtaining expectations on the
outcomes of (mutually) recursive probabilistic programs. We provide several
proof rules to derive one-- and two--sided bounds for such expectations, and
show the soundness of our wp-calculus with respect to a probabilistic pushdown
automaton semantics. We also give a wp-style calculus for obtaining bounds on
the expected runtime of recursive programs that can be used to determine the
(possibly infinite) time until termination of such programs.
