We propose a weakest-precondition-style calculus for reasoning about the expected values (pre-expectations) of mixed-sign unbounded random variables after execution of a probabilistic program. The semantics of a while-loop is well-defined as the limit of iteratively applying a functional to a zero-element just as in the traditional weakest pre-expectation calculus, even though a standard least fixed point argument is not applicable in this context. A striking feature of our semantics is that it is always well-defined, even if the expected values do not exist. Our calculus is sound and allows for invariant-based reasoning about pre-expectations of loops.
Extended Abstract: pps_mixed_sign_wp_kaminski_katoen.pdf
Authors: Benjamin Lucien Kaminski and Joost-Pieter Katoen