命令式量子程序的推理
Reasoning About Imperative Quantum Programs
Chadha、Mateus 与 Sernadas 研究命令式量子程序的逻辑推理及其与概率程序方法的联系。
论文信息（2006，Electronic Notes in Theoretical Computer Science 158:19–39）：Rohit Chadha、Paulo Mateus、Amílcar Sernadas。DOI
工作
本文研究如何为包含量子操作、经典控制和命令式结构的程序建立推理方法。它把量子程序的状态变换、概率性观察和 Hoare 风格的程序逻辑放在同一讨论中，并分析命令式程序的语义与可证明性质。论文还把问题与概率程序、量子命题逻辑和相关的量子协议研究联系起来。
主要贡献
- 为命令式量子程序的状态和控制结构提供形式推理视角。
- 讨论量子程序语义与概率谓词、Hoare 风格逻辑之间的联系。
- 将量子操作、经典命令和程序性质放进可组合的分析框架。
- 为后续量子程序验证、量子霍尔逻辑和概率量化推理提供早期参照。
局限与适用范围
论文研究的是抽象程序模型和逻辑推理，不是验证某个编译器、芯片或完整软件系统。证明依赖所选状态空间、观察语言、终止和概率语义；噪声、浮点误差、动态资源和硬件约束需要另外建模。逻辑中的可证明性也不等于所有程序性质都能自动判定。
与其他工作的关系
它与 量子最弱前置条件 共同构成早期量子程序逻辑路线：前者强调命令式程序的逻辑推理，后者强调由状态变换导出的 predicate transformer。它也承接 量子程序设计 的命令式和概率语义，并为百科中的量子霍尔逻辑与验证工具页面提供历史背景。与 通信量子进程 相比，它关注程序断言而非进程间信道通信。
原论文
Rohit Chadha, Paulo Mateus, and Amílcar Sernadas, Reasoning About Imperative Quantum Programs, Electronic Notes in Theoretical Computer Science 158, 19–39 (2006), DOI: 10.1016/j.entcs.2006.04.003.