量子关系 Hoare 逻辑

论文信息（2019，POPL/PACMPL）：Dominique Unruh。DOI；作者页面；预印本

工作

Quantum relational Hoare logic（qRHL）用于推理两段命令式量子程序的关系：如果两边输入满足某种关系，运行后输出是否仍满足对应关系。它延续概率关系 Hoare 逻辑的安全证明思路，但专门处理量子寄存器相等、量子测量和量子密码协议等问题。论文还实现了证明工具并给出安全性示例。

主要贡献

• 建立量子程序的关系 Hoare 逻辑。
• 处理量子寄存器关系与量子程序成对运行的语义挑战。
• 将逻辑用于后量子密码和量子协议安全分析。
• 提供 qRHL 证明工具和示例安全证明。

局限与适用范围

逻辑的结论依赖关系谓词、程序模型和证明规则的语义假设；工具支持不等于所有程序性质都能自动证明。它关注程序间关系和安全性质，不直接提供硬件噪声、性能或单程序所有输入上的功能正确性保证。

与其他工作的关系

qRHL 受概率关系 Hoare 逻辑启发，可与量子程序的 Floyd–Hoare 逻辑的单程序断言对照；本文不据此宣称它直接扩展 Ying 的证明系统。它与量子程序的关系证明形成互补路线。与通信量子进程相比，qRHL 强调关系规格与安全证明，而不是进程通信语义。

原论文

Dominique Unruh, Quantum Relational Hoare Logic, Proceedings of the ACM on Programming Languages 3(POPL), Article 33 (2019), DOI: 10.1145/3290346. 作者页面