带有射影断言的量子程序精细化演算

《ACM Transactions on Software Engineering and Methodology》：Refinement calculus of quantum programs with projective assertions

量子程序细化计算方法，采用正交投影作为状态断言，建立弱自由前件与强后置语义对偶体系，通过CoqQ框架形式化验证，支持模块化开发。实例涵盖Z旋转门、重复纠错码及量子伯努利工厂，并开发了QRefine原型工具。

　　

摘要

本文提出了一种专为量子程序设计的精化演算方法，该方法为量子程序的渐进式和模块化开发提供了一种结构化的途径，同时确保了整个精化过程的正确性。我们首先研究了基于量子时序语言（quantum while language）的非确定性程序的部分正确性，这类语言中包含规范语句（prescription statements）。正交投影器（orthogonal projectors）与状态希尔伯特空间（state Hilbert space）的子空间一一对应，被用作量子状态的断言。我们定义了量子程序的最弱自由前置条件（weakest liberal precondition）和最强后置条件语义（strongest postcondition semantics），并基于这两种对偶语义，引入了有助于量子程序增量开发的精化规则。所有这些规则及其正确性和完备性都通过Coq证明助手进行了形式化验证，该助手利用了CoqQ这一通用量子计算和程序验证框架。为了展示精化演算的实用性，我们通过实例进行了验证，包括实现了一个Z旋转门（Z-rotation gate）、重复纠错码（repetition error-correction code）以及量子到量子的伯努利工厂（quantum-to-quantum Bernoulli factory）。此外，我们还展示了QRefine这一基于Python的交互式原型，作为概念验证，用以证明我们方法在逐步开发正确量子程序方面的潜力。