Quantum Hoare logic (QHL) is a formal verification tool specifically designed to ensure the correctness of quantum programs. There has been an ongoing challenge to achieve a relatively complete satisfaction-based QHL with while-loop since its inception in 2006. This paper presents a solution by proposing the first relatively complete satisfaction-based QHL with while-loop. The completeness is proved in two steps. First, we establish a semantics and proof system of Hoare triples with quantum programs and deterministic assertions. Then, by utilizing the weakest precondition of deterministic assertion, we construct the weakest preterm calculus of probabilistic expressions. The relative completeness of QHL is then obtained as a consequence of the weakest preterm calculus. Using our QHL, we formally verify the correctness of Deutsch's algorithm and quantum teleportation.

翻译：量子霍尔逻辑（QHL）是一种专门设计用于确保量子程序正确性的形式化验证工具。自2006年提出以来，实现带有while循环的、相对完备的基于满足的量子霍尔逻辑一直是一个持续挑战。本文提出了一种解决方案，首次构建了带有while循环的相对完备的基于满足的量子霍尔逻辑。完备性的证明分两步进行。首先，我们建立了量子程序和确定性断言的霍尔三元组的语义和证明系统。然后，通过利用确定性断言的最弱前置条件，我们构造了概率表达式的最弱前置演算。量子霍尔逻辑的相对完备性由此作为最弱前置演算的结果而获得。利用我们的量子霍尔逻辑，我们形式化验证了多伊奇算法和量子隐形传态的正确性。