Towards a UTP-style framework to deal with probabilities

Abstract

We present an encoding of the semantics of the probabilistic guarded command language (pGCL) in the Unifying Theories of Programming (UTP) framework. Our contribution is a UTP encoding that captures pGCL programs as predicate-transformers, on predicates over probability distributions on before- and after-states: these predicates capture the same information as the models traditionally used to give semantics to pGCL; in addition our formulation allows us to de?ne a generic choice construct, that covers conditional, probabilistic and non-deterministic choice. We introduce the concept of probabilistic re?nement in this framework. This technical report gives a rigourous presentation of our framework, along with a variety of proofs and examples (including the well-known Monty Hall problem), that help to explain it.