On the Relative Completeness of Satisfaction-based Probabilistic Hoare Logic With While Loop

TL;DR

This paper introduces a new satisfaction-based probabilistic Hoare logic with While-loops, proving its relative completeness and enhancing formal reasoning about randomized programs with complex control flows.

Contribution

It establishes the first relative completeness proof for satisfaction-based PHL with While-loops and develops a new calculus using weakest preterms for probabilistic expressions.

Findings

Proves the relative completeness of the new PHL with While-loops.

Develops a semantics and proof system for probabilistic Hoare triples.

Constructs a weakest preterm calculus for probabilistic expressions.

Abstract

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.