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.