  This paper presents a wp-style calculus for obtaining bounds on the expected
run-time of probabilistic programs. Its application includes determining the
(possibly infinite) expected termination time of a probabilistic program and
proving positive almost-sure termination - does a program terminate with
probability one in finite expected time? We provide several proof rules for
bounding the run-time of loops, and prove the soundness of the approach with
respect to a simple operational model. We show that our approach is a
conservative extension of Nielson's approach for reasoning about the run-time
of deterministic programs. We analyze the expected run-time of some example
programs including a one-dimensional random walk and the coupon collector
problem.
