Probabilistic Hoare logic (PHL) is an extension of Hoare logic and is specifically useful in verifying randomized programs. It allows researchers to formally reason about the behavior of programs with stochastic elements, ensuring the desired probabilistic properties are upheld. The relative completeness of satisfaction-based PHL has been an open problem ever since the birth of the first PHL in 1979. More specifically, no satisfaction-based PHL with While-loop has been proven to be relatively complete yet. This paper solves this problem by establishing a new PHL with While-loop and prove its relative completeness. The programming language concerned in our PHL is expressively equivalent to the existing PHL systems but brings a lot of convenience in showing completeness. The weakest preterm for While-loop command reveals how it changes the probabilistic properties of computer states, considering both execution branches that halt and infinite runs. We prove the relative completeness of our PHL in two steps. We first establish a semantics and proof system of Hoare triples with probabilistic programs and deterministic assertions. Then, by utilizing the weakest precondition of deterministic assertions, we construct the weakest preterm calculus of probabilistic expressions. The relative completeness of our PHL is then obtained as a consequence of the weakest preterm calculus.

翻译：概率霍尔逻辑（PHL）是霍尔逻辑的扩展，特别适用于验证随机化程序。它使研究者能够形式化地推理具有随机元素的程序行为，确保所需的概率性质得以保持。自1979年首个PHL诞生以来，基于满足的PHL的相对完备性一直是一个悬而未决的问题。更具体地说，目前尚未有任何包含While循环的基于满足的PHL被证明是相对完备的。本文通过建立一个新的包含While循环的PHL并证明其相对完备性，解决了这一问题。我们所构建的PHL涉及的编程语言在表达能力上与现有PHL系统等价，但为证明完备性带来了诸多便利。While循环命令的最弱前置项揭示了其如何改变计算机状态的概率性质，同时考虑了会停止的执行分支和无限运行的情况。我们通过两个步骤证明PHL的相对完备性：首先建立包含概率程序和确定性断言的霍尔三元组的语义及证明系统；然后，利用确定性断言的最弱前置条件，构建概率表达式的最弱前置项演算。PHL的相对完备性作为最弱前置项演算的结果得以获得。