  An important question for a probabilistic program is whether the probability
mass of all its diverging runs is zero, that is that it terminates "almost
surely". Proving that can be hard, and this paper presents a new method for
doing so; it is expressed in a program logic, and so applies directly to source
code. The programs may contain both probabilistic- and demonic choice, and the
probabilistic choices may depend on the current state.
  As do other researchers, we use variant functions (a.k.a.
"super-martingales") that are real-valued and probabilistically might decrease
on each loop iteration; but our key innovation is that the amount as well as
the probability of the decrease are parametric.
  We prove the soundness of the new rule, indicate where its applicability goes
beyond existing rules, and explain its connection to classical results on
denumerable (non-demonic) Markov chains.
