量子霍尔逻辑

Quantum Hoare logic 将经典 Hoare triple {P} C {Q} 推广到量子程序。量子 predicate 通常不是布尔集合，而是 Hilbert 空间上的 effect：$0\preceq P\preceq I$；对态 $\rho$，$\mathrm{tr}(P\rho)$ 可解释为满足性质的权重或测量概率。命令的数学含义写为 $\llbracket C\rrbracket$，它可以是 CPTNI map，见指称语义。

Partial correctness 与 trace 项

设程序的指称语义为 trace-nonincreasing 的映射 $E=\llbracket C\rrbracket$，输入为正半定的 partial density operator $\rho$。在 Ying 论文采用的约定下，partial correctness 的条件是

最后两项是尚未终止或被语义丢弃的质量；省略它们会把条件写成 total correctness 的形式。total correctness 的三元组直接采用不带损失项的条件，并把终止要求体现在该不等式中；例如前置谓词取 $P=I$ 时，它会约束相关输入的终止，而不必声称程序对所有可能输入全局终止。若程序本身是 trace-preserving，损失项恒为零，partial 与 total 的这两个不等式一致。不同文献对谓词范围和终止约定可能有变体，使用规则前应固定语义。这里是公式说明，不声称已对具体程序完成证明。

测量分支与量子谓词

若测量后按结果分支，后继命令可对每个 classical outcome 分别验证，再依据规则合并。若 outcome 被 discard，则状态变换为 $\sum_mP_m\rho P_m$，而不能把各分支的 amplitudes 相加；对应 postcondition 也必须针对无条件混合态解释。一个简单 predicate 是 $P=\lvert1\rangle\langle1\rvert$，它测量输入落在 $\lvert1\rangle$ 的权重。与最弱前置条件配合时，可反向计算满足给定 $Q$ 的最弱 effect。

参考文献：

• D’Hondt 与 Panangaden，Quantum weakest preconditions，arXiv:quant-ph/0501157。
• Mingsheng Ying，Hoare Logic for Quantum Programs，arXiv:0906.4586。