The B-Method (B) is a formal method for development of large software systems, and is based on set theory and the predicate calculus. The semantics of B is given by the Generalised Substitution Language (GSL) invented by Abrial which gives the method a capability of reasoning about the correctness of systems.
Abrial's GSL can be modified to operate on arithmetic expressions, rather than Boolean predicates, which allows it to be applied to probabilistic programs. A new operator for probabilistic choice substitution has been added to GSL by Morgan, and we get the probabilistic Generalised Substitution Language (pGSL): a smooth extension of GSL that includes random algorithms and probabilistic systesm within its scope.
We want to examine the effect of pGSL on B's larger-scale structures: its machines: for that we suggest a notion of probabilistic machine invariants. 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.
Furthermore, we want to take these specifications and to refine them into implementations. We develop a method that can be used to develop systems with probabilistic properties from specifications to implementations. We give the definition for the consistency of the implementation with respect to the specification based on the concept of refinement.
Overall, we aim to initiate the development of a probabilistic B-Method (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 systems.