  We study a syntax for specifying quantitative "assertions" - functions
mapping program states to numbers - for probabilistic program verification. We
prove that our syntax is expressive in the following sense: Given any
probabilistic program $C$, if a function $f$ is expressible in our syntax, then
the function mapping each initial state $\sigma$ to the expected value of $f$
evaluated in the final states reached after termination of $C$ on $\sigma$
(also called the weakest preexpectation $\textit{wp} [C](f)$) is also
expressible in our syntax.
  As a consequence, we obtain a relatively complete verification system for
reasoning about expected values and probabilities in the sense of Cook: Apart
from proving a single inequality between two functions given by syntactic
expressions in our language, given $f$, $g$, and $C$, we can check whether $g
\preceq \textit{wp} [C] (f)$.
