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)，我们开发了一个仅需对经典霍尔逻辑进行最小修改的量子程序证明系统。此外，该证明系统能够有效且方便地与经典一阶逻辑结合，以验证含经典变量的量子程序。因此，对于已经熟悉经典程序验证技术的人员，量子程序验证技术的学习曲线显著降低，并且现有的经典程序验证工具也能更容易地适配于量子程序验证。