A note on expectation transformer semantics

An expectation is a function that maps program states to either a nonnegative real value, or a non-negative real-valued expression over state variables. When the program contains randomized operations, an expectation here is in fact a nonnegative random variable over the distribution induced by the reachability probability of program states. An expectation is called a post-expectation when it is to be evaluated in on final states. An expectation is called a pre-expectation if it is to be evaluated on initial states.

Intuitively, we may regard a post-expectation as a random variable representing nonnegative "rewards" of final states. One can examine the program beforehand to estimate for each initial state the expected rewards when the program runs repeatedly from there. This estimate, called the weakest pre-expectation, is a nonnegative function that maps an initial state to the expected reward over the final states starting from that state. In other words, a weakest pre-expectation evaluates to the expected value of the post-expectation over the distribution of final states produced by program executions.

Given a probabilistic program $prog$ and a post-expectation $postE$ over final states, we use $wp(prog,postE)$ to denote the weakest pre-expectation of $prog$ with respect to $postE$. As a function over state variables, $wp(prog,postE)$ maps an initial state of $prog$ to the expected value of $postE$ in the final distribution reached via executions of $prog$. In particular, $wp(prog,1)$ maps an initial state to the probability that the program will terminate from that state, and $wp(prog,[pred])$ is the probability that the program will terminate in a state satisfying predicate $pred$. (Here we use square brackets $[\cdot]$ to denote an indicator function, so that given a predicate $pred$, $[pred]$ evaluates to 1 on states satisfying $pred$ and evaluates to 0 otherwise.)

Expectations are quantitative analogue to predicates in the predicate transformer semantics; they yield expectation transformer semantics of probabilistic programs. An expectation transformer is a total function between two expectations on the states of a program. The expectation transformer $wp(prog,postE)$ gives the least expected value of $postE$ over the distribution produced by the executions of $prog$. The annotation $\langle {preE} \rangle\; prog\;\langle {postE} \rangle$ holds for total correctness if and only if \begin{equation} preE\le wp(prog,postE),\label{eq:pre-wp-post} \end{equation} where $\le$ is interpreted in a point-wise manner. In other words, $preE$ gives in each initial state a lower bound for the expected value of $postE$ on final states when $prog$ starts from that initial state.

In the special case when expectations $preE$ and $postE$ are given by $[pre]$ and $[post]$, respectively, where $pre$ and $post$ are predicates, annotation $\langle {preE} \rangle\; prog\;\langle {postE} \rangle$ is just the embedded form of a standard Hoare-triple specification $\{pre\}\; prog\;\{post\}$, i.e., we can assume the truth of $post$ after the execution of $prog$, provided $pre$ holds in the initial state. More precisely, we have \[ [pre]\le wp(prog,[post])\quad\mbox{iff}\quad pre\Rightarrow wp(prog,post). \]In this view, inequality between expectations in expectation transformer semantics can be seen as a generalization of implication between predicates in predicate transformer semantics.

Reference

McIver, Annabelle, and Charles Carroll Morgan. "Abstraction, refinement and proof for probabilistic systems." Springer, 2006.