In this paper, we present a Hoare-style logic for reasoning about quantum programs with classical variables. Our approach offers several improvements over previous work: (1) Enhanced expressivity of the programming language: Our logic applies to quantum programs with classical variables that incorporate quantum arrays and parameterised quantum gates, which have not been addressed in previous research on quantum Hoare logic, either with or without classical variables. (2) Intuitive correctness specifications: In our logic, preconditions and postconditions for quantum programs with classical variables are specified as a pair consisting of a classical first-order logical formula and a quantum predicate formula (possibly parameterised by classical variables). These specifications offer greater clarity and align more closely with the programmer's intuitive understanding of quantum and classical interactions. (3) Simplified proof system: By introducing a novel idea in formulating a proof rule for reasoning about quantum measurements, along with (2), we develop a proof system for quantum programs that requires only minimal modifications to classical Hoare logic. Furthermore, this proof system can be effectively and conveniently combined with classical first-order logic to verify quantum programs with classical variables. As a result, the learning curve for quantum program verification techniques is significantly reduced for those already familiar with classical program verification techniques, and existing tools for verifying classical programs can be more easily adapted for quantum program verification.

翻译：本文提出一种用于推理含经典变量量子程序的霍尔风格逻辑系统。与既往研究相比，本方法在以下方面取得突破：(1) 编程语言表达能力提升：本逻辑适用于包含量子数组与参数化量子门的经典变量量子程序——这在先前量子霍尔逻辑研究（无论是否包含经典变量）中均未涉及；(2) 直观的正确性规约：本逻辑中，含经典变量量子程序的前置条件与后置条件被定义为经典一阶逻辑公式与（可能经经典变量参数化的）量子谓词公式的二元组，这种规约方式更清晰且更贴近程序员对量子-经典交互的直觉理解；(3) 简化的证明系统：通过引入量子测量推理证明规则的新颖构思，结合上述第(2)点，我们建立了仅需对经典霍尔逻辑进行最小化修改的量子程序证明系统。此外，该证明系统可与经典一阶逻辑有效便捷地结合，用于验证含经典变量的量子程序。对于已掌握经典程序验证技术的研究者而言，量子程序验证技术的学习曲线由此显著降低，且现有经典程序验证工具可更便捷地适配量子程序验证场景。