论文标题
带经典变量的量子hoare逻辑
Quantum Hoare logic with classical variables
论文作者
论文摘要
Hoare Logic提供了一种面向语法的方法来推理程序正确性，并已被证明有效地验证了经典和概率的程序。量子Hoare逻辑的现有建议要么缺乏完整性或仅支持量子变量，因此限制了它们在实际使用中的能力。在本文中，我们为简单的语言提出了一种量子hoare逻辑，涉及古典变量和量子变量。它的健全性和相对完整性被证明是用语言编写的量子程序的部分和总正确性。值得注意的是，借助古典量子状态和相应断言的新颖定义，逻辑系统非常简单，并且与古典程序的传统Hoare逻辑相似。此外，为了简化实际应用中的推理，提供了辅助证明规则，该规则支持在断言的经典部分中支持标准逻辑操作，以及量子部分中的超级操作器应用程序。最后，一系列实用的量子算法，尤其是Shor的整个算法，已正式验证以显示逻辑的有效性。
Hoare logic provides a syntax-oriented method to reason about program correctness and has been proven effective in the verification of classical and probabilistic programs. Existing proposals for quantum Hoare logic either lack completeness or support only quantum variables, thus limiting their capability in practical use. In this paper, we propose a quantum Hoare logic for a simple while language which involves both classical and quantum variables. Its soundness and relative completeness are proven for both partial and total correctness of quantum programs written in the language. Remarkably, with novel definitions of classical-quantum states and corresponding assertions, the logic system is quite simple and similar to the traditional Hoare logic for classical programs. Furthermore, to simplify reasoning in real applications, auxiliary proof rules are provided which support standard logical operation in the classical part of assertions, and of super-operator application in the quantum part. Finally, a series of practical quantum algorithms, in particular the whole algorithm of Shor's factorisation, are formally verified to show the effectiveness of the logic.
