Karen Seidel, Carroll Morgan and Annabelle McIver
March 1996, 27pp.
Probabilistic predicate transformers provide a semantics for an imperative programming language which contains a construct for probabilistic choice: the language can be used to describe sequential randomised algorithms; and the semantics makes it possible in principle to prove their correctness and efficiency, that is to calculate the probability of establishing a desired result and the expected number of steps needed to do so.
This paper gives a brief and to some extent informal introduction to the definition, properties and use of probabilistic predicates and their transformers. The first part explains the intuition behind them and applies them to some examples. The second part concentrates on their properties, the probabilistic "healthiness conditions" that generalise those of Dijkstra for ordinary predicate transformers: they are important both theoretically (for the characterisation of subspaces) and practically (for the development of proof rules).
The paper concludes with an overview of further material on the probabilistic predicate transformers.