Programming Research Group
Technical Report TR-4-95
Probabilistic predicate transformers
Carroll Morgan,
Annabelle McIver,
Karen Seidel and
J W Sanders
February 1995, 37pp.
Abstract
Predicate transformers facilitate reasoning about imperative programs,
including those exhibiting demonic non-deterministic choice.
Probabilistic predicate transformers extend that facility to programs
containing probabilistic choice, so that one can in principle determine
not only whether a program is guaranteed to establish a certain result,
but also its probability of doing so.
We bring together independent work of Claire Jones and Jifeng He,
showing how their constructions can be made to correspond; from that
link between a predicate-based and a relation-based view of
probabilistic execution we are able to propose "probabilistic
healthiness conditions", generalising those of Dijkstra for ordinary
predicate transformers.
The associated calculus seems suitable for exploring further the
rigorous derivation of imperative probabilistic programs.
Keywords
Probability , predicate transformers, non-determinism, verification,
refinement, imperative programming, program derivation, Galois
connection.
This paper is available as a 93,400 byte
gzipped PostScript file.