最弱前置条件

对程序 $C$ 和后置量子谓词 $Q$，在总正确性约定下，weakest precondition $\mathrm{wp}_C(Q)$ 是满足后置条件所需的最弱输入谓词。若 $E=\llbracket C\rrbracket$ 是对 partial density operators 的线性映射，常用伴随映射定义

这一定义把量子霍尔逻辑中的总正确性条件转化为可组合的反向计算。对可能不终止的程序，weakest liberal precondition（$\mathrm{wlp}$）对应 partial correctness；若 $E$ 是 trace-nonincreasing 映射，则

于是 $\mathrm{tr}(\mathrm{wlp}_C(Q)\rho)=\mathrm{tr}(QE(\rho))+\mathrm{tr}(\rho)-\mathrm{tr}(E(\rho))$，其中最后两项正是未终止或损失的质量。

例子：门与测量

若 $C$ 是 unitary $U$，则

因此对 $Q=\lvert1\rangle\langle1\rvert$ 和 $U=X$，最弱前置条件是 $\lvert0\rangle\langle0\rvert$。若测量用 Kraus 算子 $M_m$ 描述并 discard outcome，

如果 outcome 被保留并用于 classical control，则后置空间应包含 classical register，不能直接套用丢弃分支的式子。

边界与使用方式

“最弱”依赖谓词偏序 $P\preceq P'$；在有限维 effect 上通常按半正定序比较。循环或递归需要不动点，非终止会影响 trace 项和 total correctness 的解释。离散数学中的布尔前置条件也不能直接替代 quantum effect。该方法提供推理框架，不代表每个程序的 wp 都能自动算出闭式表达式；数值近似还会引入误差界问题。相关推广包括 generalised weakest preconditions 与带 classical variables 的模型。

参考文献：

• D’Hondt 与 Panangaden，Quantum Weakest Preconditions，arXiv:quant-ph/0501157。
• Roman Gielerak 与 Marek Sawerwain，Generalised quantum weakest preconditions，arXiv:0710.5239。