量子程序的 Floyd–Hoare 逻辑
Floyd–Hoare Logic for Quantum Programs
Ying 建立覆盖部分正确性和完全正确性的量子 Floyd–Hoare 逻辑，并证明相对完备性。
论文信息（2011，TOPLAS 33(6)，Article 19，pp. 1–49）：Mingsheng Ying。DOI；arXiv:0906.4586
工作
本文把经典 Floyd–Hoare 逻辑的三元组思想推广到量子程序。量子断言用描述测量性质的算子表示，程序语句通过推理规则改变断言；体系同时讨论 partial correctness 与 total correctness。论文还使用量子最弱前置条件来说明系统的相对完备性，即在给定语义和断言表达能力的前提下，语义上成立的性质可以由规则推导。
主要贡献
- 建立量子程序的 Floyd–Hoare 三元组和推理规则。
- 同时覆盖部分正确性与完全正确性。
- 处理量子操作、测量和循环等程序构造的断言推理。
- 以量子最弱前置条件为基础证明相对完备性。
局限与适用范围
相对完备性依赖断言语言能够表达所需的最弱前置条件，并不意味着实际证明可以自动生成。循环仍需要合适的不变量与终止论证；体系的量子模型、经典变量、非终止和噪声假设需要明确。形式逻辑的证明也不等同于具体编译器或硬件实现已经正确。
与其他工作的关系
本文承接 量子最弱前置条件 的 predicate-transformer 视角，并把它组织为可组合的程序逻辑。它与 命令式量子程序的推理 都关注命令式量子程序，但本文更系统地给出 Floyd–Hoare 规则与相对完备性。量子循环的语义可参见 量子循环程序，工具层面的限制见验证方法与工具。
原论文
Mingsheng Ying, Floyd–Hoare Logic for Quantum Programs, ACM Transactions on Programming Languages and Systems 33(6), Article 19, 1–49 (2011), DOI: 10.1145/2049706.2049708. arXiv:0906.4586