Advertisement

Development via Refinement in Probabilistic B — Foundation and Case Study

  • Thai Son Hoang
  • Zhendong Jin
  • Ken Robinson
  • Annabelle McIver
  • Carroll Morgan
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3455)

Abstract

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 [8]. 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.

Keywords

Probability program correctness generalised substitutions weakest preconditions B randomised algorithms refinement 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)zbMATHCrossRefGoogle Scholar
  2. 2.
    Abrial, J.-R., Cansell, D., Mery, D.: A mechanically proved and incremental development of IEEE 1394 firewire tree identify protocol. Formal Aspects of Computing 14(3), 215–227 (2003)CrossRefGoogle Scholar
  3. 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
  4. 4.
    Back, R.-J., Von Wright, J.: Refinement Calculus, a Systematic Introduction. Springer, New york (1998)zbMATHGoogle Scholar
  5. 5.
    B Core(UK) Ltd. B Toolkit, http://www.b-core.com
  6. 6.
    Fidge, C.J., Shankland, C.: But what if I don’t want to wait forever? Formal Aspects of Computing 14(3), 281–294 (2003)CrossRefGoogle Scholar
  7. 7.
    Gries, D.: A note on a standard strategy for developing loop invariants and loops. Science of Computer Programming 2, 207–214 (1984)CrossRefGoogle Scholar
  8. 8.
    Hoang, T.S., Jin, Z., Robinson, K., McIver, A., Morgan, C.: Probabilistic Invariants for Probabilistic Machines. In: Bert, D., P. Bowen, J., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 240–259. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  9. 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. 10.
    INRIA. The Coq proof assistant, http://coq.inria.fr/
  11. 11.
    McIver, A., Morgan, C., Hoang, T.S.: Probabilistic termination in B. In: Bert, D., Bowen, J. P., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 216–239. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  12. 12.
    Morgan, C.: The specification statement. ACM Transactions on Programming Languages and Systems 10(3) (July 1988) Reprinted in [18]Google Scholar
  13. 13.
    Morgan, C.: Programming from Specifications. Prentice-Hall, Englewood Cliffs (1994), web.comlab.ox.ac.uk/oucl/publications/books/PfS zbMATHGoogle Scholar
  14. 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
  15. 15.
    Morgan, C.: The Generalised Substitution Language extended to probabilistic programs. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, p. 9. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  16. 16.
    Morgan, C., McIver, A.: Abstraction, Refinement and Proof for Probabilistic Systems. In: Monographs in Computer Science. Springer, Heidelberg (2004)Google Scholar
  17. 17.
    Morgan, C., Robinson, K.: Specification Statements and Refinements. In: On the Refinement Calculus, pp. 23–45. Springer, Heidelberg (1992)Google Scholar
  18. 18.
    Morgan, C., Vickers, T. (eds.): On the Refinment Calculus. FACIT Series in Computer Science. Springer, Berlin (1994)Google Scholar
  19. 19.
    Morris, J.M.: A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming 9(3), 287–306 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press, Cambridge (1995)zbMATHGoogle Scholar
  21. 21.
    White, N.: Probabilistic Specification and Refinement. Master’s thesis, Keble College (September 1996)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Thai Son Hoang
    • 1
    • 2
  • Zhendong Jin
    • 1
  • Ken Robinson
    • 1
    • 2
  • Annabelle McIver
    • 3
  • Carroll Morgan
    • 1
  1. 1.School of Computer Science & EngineeringUniversity of New South WalesAustralia
  2. 2.National ICTAustralia
  3. 3.Department of ComputingMacquarie UniversityAustralia

Personalised recommendations