最弱前期望

布尔后置条件只问成功与否，后期望允许给成功结果不同奖励。反向计算把“最终能拿多少钱”变成“从当前状态开始平均能拿多少钱”。概率分支因此使用加权平均，而不是逻辑合取或最小值。

最小不动点不可省略。一个循环方程可能有很多解，只有从有限终止执行累积出的最小解符合这里的非终止约定。

顺序替换要从最后一行开始 ​

程序以概率 $1/3$ 执行 $x:=2$，否则 $x:=5$，随后执行 $x:=x+1$。取最终奖励 $f(x)=x^2$。先穿过末行，得 $(x+1{)}^2$；再穿过分支，得

若先把 $x$ 的平均值算成 $4$，再算 $(4+1{)}^2=25$，就错把非线性奖励作用于均值。规则保留了奖励与分布之间正确的顺序。

输出期望与条件输出均值不同 ​

程序以概率 $1/4$ 返回 $8$，其余永远循环。则 $\mathrm{wp}[C](x)=2$，$\mathrm{wp}[C](1)=1/4$。若条件于终止，平均输出才是 $2/(1/4)=8$。wp 本身没有偷偷做这个除法。

对事件 $A$，$\mathrm{wp}[C]([A])$ 是终止且落入 $A$ 的概率；对 $1$ 则是终止概率。确定性总正确性下的 最弱前置条件公理库最弱前置条件Weakest precondition保证程序建立给定后置条件的最弱状态谓词。可以看作相应指示函数的特例，但部分正确性的 wlp 有不同非终止约定。

相同不动点方程可以有不同候选解 ​

对永不退出的 while true do skip，${\mathrm{\Phi }}_f(X)=X$，每个函数都是不动点，最小者为零，所以 wp 为零。对每轮以概率 $p>0$ 结束、结束奖励为一的循环，标量方程为

零起点迭代得 $x_n=1-(1-p{)}^n$，极限为一。若 $p=0$，方程又变成 $x=x$，最小解却是零，不能直接除以 $p$ 延续前面的计算。

wp 单调：$f\le g$ 蕴涵 $\mathrm{wp}[C](f)\le \mathrm{wp}[C](g)$。在本页没有非确定选择的语义下，它还对非负奖励线性；循环依靠单调收敛定理公理库单调收敛定理Monotone convergence theorem非负可测函数单调递增时，积分极限等于极限函数积分。把有限展开的等式传给极限。

概率循环不变式公理库概率循环不变式与期望界Probabilistic loop invariant · Expectation invariant以循环特征函数的不等式证明输出期望界，展示上界归纳、下界反例，以及几乎必停和有界性怎样消除尾项。用 ${\mathrm{\Phi }}_f(I)\le I$ 提供上界；下界不能只把不等号反过来。期望运行时间变换器公理库期望运行时间变换器Expected runtime transformer · ERT calculus给概率程序逐项计费并反向组合期望成本，用几何循环算出守卫检查的额外开销，区分 ert 与 wp。则另加执行成本，不能只把 wp 的后期望换成一就得到运行时间。