Development via Refinement in Probabilistic B — Foundation and Case Study
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.
KeywordsProbability program correctness generalised substitutions weakest preconditions B randomised algorithms refinement
Unable to display preview. Download preview PDF.
- 3.Back, R.-J.: On the correctness of refinement in program development. PhD thesis, Department of Computer Science, University of Helsinki, Report A-1978-4 (1978)Google Scholar
- 5.B Core(UK) Ltd. B Toolkit, http://www.b-core.com
- 9.Hoang, T.S., Jin, Z., Robinson, K., McIver, A., Morgan, C.: Proofs of the Min-Cut development. (April 2004), http://www.cse.unsw.edu.au/~htson/b/minCutProofs.pdf
- 10.INRIA. The Coq proof assistant, http://coq.inria.fr/
- 12.Morgan, C.: The specification statement. ACM Transactions on Programming Languages and Systems 10(3) (July 1988) Reprinted in Google Scholar
- 14.Morgan, C.: Proof rules for probabilistic loops. In: Cooke, H.J.J., Wallis, P. (eds.) Proceedings of the BCS-FACS 7th Refinement Workshop, July 1996. Workshops in Computing, Springer, Heidelberg (1996)Google Scholar
- 16.Morgan, C., McIver, A.: Abstraction, Refinement and Proof for Probabilistic Systems. In: Monographs in Computer Science. Springer, Heidelberg (2004)Google Scholar
- 17.Morgan, C., Robinson, K.: Specification Statements and Refinements. In: On the Refinement Calculus, pp. 23–45. Springer, Heidelberg (1992)Google Scholar
- 18.Morgan, C., Vickers, T. (eds.): On the Refinment Calculus. FACIT Series in Computer Science. Springer, Berlin (1994)Google Scholar
- 21.White, N.: Probabilistic Specification and Refinement. Master’s thesis, Keble College (September 1996)Google Scholar