## Abstract

The B Method [1] does not currently handle probability. We add it in a limited form, concentrating on "almost-certain" properties which hold with probability one; and we address briefly the implied modifications to the programs that support B. The Generalised Substitution Language is extended with a binary operator ⊕ representing "abstract probabilistic choice", so that the substitution prog_{1} ⊕ prog_{2} means roughly "choose between prog_{1} and prog_{2} with some probability neither one nor zero". We then adjust B's proof rule for loops - specifically, the variant rule - so that in many cases it is possible to prove "probability-one" correctness of programs containing the new operator, which was not possible in B before, while remaining almost entirely within the original Boolean logic. Applications include probabilistic algorithms such as the IEEE 1394 Root Contention Protocol ("FireWire") [9] in which a probabilistic "symmetry-breaking" strategy forms a key component of the design.

Original language | English |
---|---|

Pages (from-to) | 216-239 |

Number of pages | 24 |

Journal | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |

Volume | 2651 |

Publication status | Published - 2003 |