Please use this identifier to cite or link to this item: http://hdl.handle.net/1959.14/161030
9 Visitors11 Hits0 Downloads
Development via refinement in probabilistic B — foundation and case study
International Conference of B and Z Users (4th : 2005) (13 - 15 April 2005 : Guildford, England)
Treharne, Helen; King, Steve; Henson, Martin and Schneider, Steve;. ZB 2005 : formal specification and development in Z and B : 4th International Conference of B and Z Users, Guildford, UK, April 13-15, 2005 : proceedings, p.355-373
In earlier work, we introduced probability to the B by providing a probabilistic choice substitution and by extending B’s semantics to incorporate its meaning . This, a first step, allowed probabilistic programs to be written and reasoned about within B. This paper extends the previous work into refinement within B. To allow probabilistic specification and development within B, we must add a probabilistic specification substitution; and we must determine the rules and techniques for its rigorous refinement into probabilistic code. Implementation in B frequently contains loops. We generalise the standard proof obligation rules for loops giving a set of rules for reasoning about the correctness of probabilistic loops. We present a small case-study that uses those rules, the randomised Min-Cut algorithm.