一句话：提出可处理混合符号无界随机变量期望的概率程序最弱前置期望演算，保证语义总良定义且可靠。
本文为概率程序引入一种最弱前置条件风格的演算，用于推理程序执行后混合符号、无界随机变量的期望值（pre-expectations）。传统最弱前置期望演算通常依赖最小不动点，但混合符号期望可能不存在，标准论证不再适用。作者将 while 循环语义定义为对零元素迭代应用泛函的极限，并证明该语义总是良定义，即使相关期望值不存在。文中证明该演算具有可靠性并支持组合推理，还提出基于不变式的方法来推理循环的 pre-expectations。该工作扩展了概率程序最弱前置期望语义的适用范围。
We present 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 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 our semantics. A striking feature of our semantics is that it is always well-defined, even if the expected values do not exist. We show that the calculus is sound and allows for compositional reasoning. Furthermore, we present an invariant-based approach for reasoning about pre-expectations of loops.