Verifying the functional correctness of programs with both classical and quantum constructs is a challenging task. The presence of probabilistic behaviour entailed by quantum measurements and unbounded while loops complicate the verification task greatly. We propose a new quantum Hoare logic for local reasoning about probabilistic behaviour by introducing distribution formulas to specify probabilistic properties. We show that the proof rules in the logic are sound with respect to a denotational semantics. To demonstrate the effectiveness of the logic, we formally verify the correctness of non-trivial quantum algorithms including the HHL and Shor's algorithms.

翻译：验证同时包含经典和量子结构的程序的功能正确性是一项具有挑战性的任务。量子测量所蕴含的概率行为以及无界while循环极大地复杂化了验证工作。我们提出了一种新的量子Hoare逻辑，通过引入分布公式来规范概率属性，从而对概率行为进行局部推理。我们证明了该逻辑中的证明规则相对于指称语义是可靠的。为了展示该逻辑的有效性，我们正式验证了包括HHL算法和Shor算法在内的非平凡量子算法的正确性。