Probabilistic program verification in the style of the unifying theories of programming

Abstract

We present a novel framework to reason on programs based on probability distributions on the state space of a program: they are functions from program states to real numbers in the range [0..1], which can be used to represent the probability of a program being in that state. Such framework can be used to provide an elegant semantics in the style of UTP to a variety of programming languages using both probabilistic and nondeterministic constructs: the use of probability distributions allows us to give programs a semantics which is based on homogeneous relations. The behaviour of probabilistic nondeterministic programs is treated algebraically via this framework, and as a result it is straightforward to derive algebraic expressions for the probability of some properties to hold for a given program. Moreover our framework unifies all of the different kinds of choice under a single “generic choice” construct, and the usual choice constructs (disjunction, conditional choice, probabilistic choice, and nondeterministic choice) can be viewed as some of its specific instances. Later on we will discuss also other possible specific instances (namely conditional probabilistic choice, switching probabilistic choice, conditional nondeterministic choice, nondeterministic probabilistic choice, and fair nondeterministic choice). The use of probability allows us to introduce the notion of probabilistic refinement, which generalises the traditional one: this is important in view of formal verification of probabilistic properties of programs via refinement-based techniques.