Skip to main content
SpringerLink
Log in

Chorus Angelorum

  • Conference paper
B 2007: Formal Specification and Development in B (B 2007)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 4355))

Included in the following conference series:

Abstract

We extend B’s GSL by introducing new operators for angelic choice, thus widening its application from its original domain of conjunctive computations to that of monotonic ones in general. We explore the impact of this on our theory of substitutions [6], discovering two dual new normal forms for our new substitutions which we exploit to formulate two new first-order tests of refinement between them.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)

    Book  MATH  Google Scholar 

  2. Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, New York (1998)

    MATH  Google Scholar 

  3. Back, R.J.R., von Wright, J.: Combining angels, demons and miracles in program specifications. Theoretical Computer Science 100, 365–383 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  4. Cavalcanti, A., Woodcock, J.C.P., Dunne, S.E.: Angelic nondeterminism in the unifying theories of programming. Formal Aspects of Computing 18(3), 288–307 (2006)

    Article  MATH  Google Scholar 

  5. Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, Berlin (1990)

    MATH  Google Scholar 

  6. Dunne, S.E.: A theory of generalised substitutions. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002: Formal Specification and Development in Z and B. LNCS, vol. 2272, pp. 270–290. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  7. Gardiner, P.H.B., Morgan, C.C.: Data refinement of predicate transformers. Theoretical Computer Science 87, 143–162 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  8. Gardiner, P.H.B., Morgan, C.C.: A single complete rule for data refinement. Formal Aspects of Computing 5, 367–382 (1993)

    Article  MATH  Google Scholar 

  9. Hehner, E.C.R.: Bunch theory: a simple set theory for computer science. Information Processing Letters 12(1), 26–30 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  10. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)

    MATH  Google Scholar 

  11. Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)

    Google Scholar 

  12. Jagaeesan, R., Shanbhogue, V., Saraswat, V.: Angelic nondeterminism in concurrent constraint programming, Xerox technical report (1991)

    Google Scholar 

  13. Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice-Hall, Englewood Cliffs (1990)

    MATH  Google Scholar 

  14. Martin, A.P., Gardiner, P.H.B., Woodcock, J.C.P.: A tactical calculus. Formal Aspects of Computing 8(4), 479–489 (1996)

    Article  MATH  Google Scholar 

  15. Martin, C.E., Curtis, S.A., Rewitzky, I.: Modelling nondeterminism. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 228–251. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  16. Rewitzky, I.: Binary multirelations. In: de Swart, H., Orłowska, E., Schmidt, G., Roubens, M. (eds.) Theory and Applications of Relational Structures as Knowledge Instruments. LNCS, vol. 2929, pp. 259–274. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  17. Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1998)

    Google Scholar 

  18. Ward, N., Hayes, I.J.: Applications of angelic nondeterminism. In: Bailes, P.A. (ed.) Proc. of the 6th Australian Software Engineering Conference (ASWEC 1991), pp. 391–404. Australian Computer Society (1991)

    Google Scholar 

  19. Woodcock, J., Davies, J.: Using Z: Specification, Refinement and Proof. Prentice-Hall, Englewood Cliffs (1996)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computing, University of Teesside, Middlesbrough, TS1 3BA, UK

    Steve Dunne

Authors
  1. Steve Dunne
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. LIFC, Université de Franche-Comté, 16, route de Gray, F-25030, Besançon Cedex, France

    Jacques Julliand

  2. LIFC – TFC Team, 16 route de Gray, F-25030, Besançon

    Olga Kouchnarenko

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dunne, S. (2006). Chorus Angelorum. In: Julliand, J., Kouchnarenko, O. (eds) B 2007: Formal Specification and Development in B. B 2007. Lecture Notes in Computer Science, vol 4355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11955757_5

Download citation

  • DOI: https://doi.org/10.1007/11955757_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-68760-3

  • Online ISBN: 978-3-540-68761-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation