J.I. den Hartog and E.P. de Vink
Verifying probabilistic programs using a Hoare-like logic

Probability, be it inherent or explicitly introduced, has become an
important issue in the verification of many programs.  In this paper
we study a formalism which allows reasoning about programs which can
%make probabilistic decisions.  act probabilistically.  To describe
probabilistic programs a basic programming language with an operator
for probabilistic choice is introduced and a denotational semantics is
given for this language.  To specify properties of probabilistic
programs, standard first order logic predicates are insufficient, so a
notion of probabilistic predicates are introduced.  A Hoare-style
proof system to check properties of probabilistic programs is given.
The proof system for a sublanguage is shown to be correct and
complete; the properties that can be derived are exactly the valid
properties.  Finally some typical examples illustrate the use of the
probabilistic predicates and the proof system.