This article presents a wp-style calculus for obtaining bounds on the expected
runtime of randomized algorithms. Its application includes determining the
(possibly infinite) expected termination time of a randomized algorithm 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 runtime 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 runtime of
deterministic programs. We analyze the expected runtime of some example
programs including the coupon collector's problem, a one-dimensional random
walk and a randomized binary search.