Skip to main content
SpringerLink
Log in

The generalised substitution language extended to probabilistic programs

  • Conference paper
  • First Online:
B’98: Recent Advances in the Development and Use of the B Method (B 1998)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1393))

Included in the following conference series:

Abstract

Let predicate P be converted from Boolean to numeric type by writing 〈P〉, with 〈false〉 being 0 and 〈true〉 being 1, so that in a degenerate sense 〈P〉 can be regarded as ‘the probability that P holds in the current state’. Then add explicit numbers and arithmetic operators, to give a richer language of arithmetic formulae into which predicates are embedded by 〈·〉.

Abrial's generalised substitution language GSL can be applied to arithmetic rather than Boolean formulae with little extra effort. If we add a new operator p⊕ for probabilistic choice, it then becomes ‘pGSL’: a smooth extension of GSL that includes random algorithms within its scope.

The work is supported by the EPSRC.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J.-R. Abrial. The B-Book. Cambridge University Press, 1996.

    Google Scholar 

  2. E.W. Dijkstra. A Discipline of Programming. Prentice Hall International, Englewood Cliffs, N.J., 1976.

    MATH  Google Scholar 

  3. Yishai A. Feldman. A decidable prepositional dynamic logic with explicit probabilities. Information and Control, 63:11–38, 1984.

    Article  MATH  MathSciNet  Google Scholar 

  4. Yishai A. Feldman and David Harel. A probabilistic dynamic logic. J. Computing and System Sciences, 28:193–215, 1984.

    Article  MATH  MathSciNet  Google Scholar 

  5. Jifeng He, K. Seidel, and A. K. McIver. Probabilistic models for the guarded command language. Science of Computer Programming, 28:171–192, 1997.

    Article  MATH  MathSciNet  Google Scholar 

  6. C. Jones. Probabilistic nondeterminism. Monograph ECS-LFCS-90-105, Edinburgh Univ. Edinburgh, U.K., 1990. (PhD Thesis).

    Google Scholar 

  7. C. Jones and G. Plotkin. A probabilistic powerdomain of evaluations. In Proceedings of the IEEE 4th Annual Symposium on Logic in Computer Science, pages 186–195, Los Alamitos, Calif., 1989. Computer Society Press.

    Google Scholar 

  8. D. Kozen. A probabilistic PDL. In Proceedings of the 15th ACM Symposium on Theory of Computing, New York, 1983. ACM.

    Google Scholar 

  9. Annabelle McIver and Carroll Morgan. Probabilistic predicate transformers: part 2. Technical Report PRG-TR-5-96, Programming Research Group, March 1996. Revised version to be submitted for publication under the title Demonic, angelic and unbounded probabilistic choices in sequential programs.

    Google Scholar 

  10. Annabelle McIver and Carroll Morgan. Partial correctness for probabilistic demonic programs. Technical Report PRG-TR-35-97, Programming Research Group, 1997.

    Google Scholar 

  11. Annabelle McIver, Carroll Morgan, and Elena Troubitsyna. The probabilistic steam boiler: a case study in probabilistic data refinement. In preparation, 1997.

    Google Scholar 

  12. C. C. Morgan. The specification statement. ACM Transactions on Programming Languages and Systems, 10(3), July 1988. Reprinted in [14].

    Google Scholar 

  13. C. C. Morgan. Proof rules for probabilistic loops. In He Jifeng, John Cooke, and Peter Wallis, editors, Proceedings of the BCS-FACS 7th Refinement Workshop, Workshops in Computing. Springer Verlag, July 1996.

    Google Scholar 

  14. C. C. Morgan and T. N. Vickers, editors. On the Refinement Calculus. FACIT Series in Computer Science. Springer-Verlag, Berlin, 1994.

    Google Scholar 

  15. Carroll Morgan, Annabelle McIver, and Karen Seidel. Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems, 18(3):325–353, May 1996.

    Article  Google Scholar 

  16. J. M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9(3):287–306, December 1987.

    Article  MATH  MathSciNet  Google Scholar 

  17. Rajeev Motwani and Prabhakar Raghavan. Randomized Algorithms. Cambridge University Press, 1995.

    Google Scholar 

  18. G. Nelson. A generalization of Dijkstra's calculus. ACM Transactions on Programming Languages and Systems, 11(4):517–561, October 1989.

    Article  Google Scholar 

  19. K. Seidel, C. C. Morgan, and A. K. McIver. An introduction to probabilistic predicate transformers. Technical Report PRG-TR-6-96, Programming Research Group, February 1996. Revised version to be submitted for publication under the title Probabilistic Imperative Programming: a Rigorous Approach.

    Google Scholar 

  20. M. Sharir, A. Pnueli, and S. Hart. Verification of probabilistic programs. SIAM Journal on Computing, 13(2):292–314, May 1984.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Programming Research Group, Oxford University, UK

    Carroll Morgan

Authors
  1. Carroll Morgan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Didier Bert

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Morgan, C. (1998). The generalised substitution language extended to probabilistic programs. In: Bert, D. (eds) B’98: Recent Advances in the Development and Use of the B Method. B 1998. Lecture Notes in Computer Science, vol 1393. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0053351

Download citation

  • DOI: https://doi.org/10.1007/BFb0053351

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64405-7

  • Online ISBN: 978-3-540-69769-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation