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. We study a formalism which allows reasoning about programs which can 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.