  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.
