量子程序的霍尔逻辑
Hoare Logic for Quantum Programs
摘要：
Hoare逻辑是经典程序公理化语义的基础，它为经典程序的正确性推理提供了有效的证明技术。为了提供类似的量子程序验证技术，并建立一个量子计算机编程方法的逻辑基础，我们开发了一个完整的霍尔逻辑的部分和全部正确的量子程序。通过利用量子程序的最弱前提和最弱自由前提的力量，证明了该逻辑是（相对）完备的。
英文摘要：
Hoare logic is a foundation of axiomatic semantics of classical programs and it provides effective proof techniques for reasoning about correctness of classical programs. To offer similar techniques for quantum program verification and to build a logical foundation of programming methodology for quantum computers, we develop a full-fledged Hoare logic for both partial and total correctness of quantum programs. It is proved that this logic is (relatively) complete by exploiting the power of weakest preconditions and weakest liberal preconditions for quantum programs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
