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循环极大地增加了验证的复杂性。我们提出了一种新的量子霍尔逻辑，通过引入分布公式来指定概率属性，从而实现对概率行为的局部推理。我们证明了该逻辑中的证明规则相对于指称语义是完备的。为了展示该逻辑的有效性，我们形式化验证了包括HHL和Shor算法在内的非平凡量子算法的正确性。