Abrial's Generalised Substitution Language (GSL) can be modified to operate on arithmetic expressions, rather than Boolean predicates, which allows it to be applied to probabilistic programs. We add a new operator probabilistic choice to GSL, and we get the probabilistic Generalised Substitution Language (pGSL): a smooth extension of GSL that includes random algorithms within its scope.
In this paper we begin to examine the effect of pGSL on B's larger-scale structures: its machines. In particular, we suggest a notion of probabilistic machine invariant. We show how these invariants interact with pGSL, at a fine-grained level; and at the other extreme we investigate how they affect our general understanding ``in the large'' of probabilistic machines and their behaviour.
Overall, we aim to initiate the development of probabilistic B (pB), complete with a suitable probabilistic Abstract Machine Notation (pAMN) . We discuss the practical extension of the B-Toolkit to support pB, and we give examples to show how pAMN can be used to express and reason about probabilistic properties of a system.
Keywords: Probability, program correctness, generalised substitutions, weakest preconditions, B, probabilistic algorithms.