Skip to main content
SpringerLink
Log in

Understanding, Explaining, and Deriving Refinement

  • Chapter
  • First Online:
Book cover From Astrophysics to Unconventional Computation

Part of the book series: Emergence, Complexity and Computation ((ECC,volume 35))

Abstract

Much of what drove us in over twenty years of research in refinement, starting with Z in particular, was the desire to understand where refinement rules came from. The relational model of refinement provided a solid starting point which allowed the derivation of Z refinement rules. Not only did this explain and verify the existing rules—more importantly, it also allowed alternative derivations for different and generalised notions of refinement. In this chapter, we briefly describe the context of our early efforts in this area and Susan Stepney’s role in this, before moving on to the motivation and exploration of a recently developed primitive model of refinement: concrete state machines with anonymous transitions.

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 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover 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

Notes

  1. 1.

    Our little joke was to call this the “every sperm is sacred” principle, in reference to Monty Python.

  2. 2.

    One of our most enlightening paper rejections was one for a 1990s ZUM conference, where we had argued the opposite, namely that data refinement could introduce non-determinism, but a reviewer explained how this was entirely illusory, as such non-determinism could never be made visible in external observations. Of course this holds particularly for formal methods like Z where the final refinement outcome is only beholden to the initial specification and not to any detail introduced along the way like it is in for example Event-B [2], where refinement of deterministic systems can indeed be entirely meaningful.

References

  1. Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci. 2(82), 253–284 (1991)

    Article  MathSciNet  Google Scholar 

  2. Abrial, J.R.: Modelling in Event-B. CUP, Cambridge (2010)

    Book  Google Scholar 

  3. Ainsworth, M., Cruickshank, A.H., Wallis, P.J.L., Groves, L.J.: Viewpoint specification and Z. Inf. Softw. Technol. 36(1), 43–51 (1994)

    Article  Google Scholar 

  4. Back, R.J.R., Kurki-Suonio, R.: Distributed cooperation with action systems. ACM Trans. Program. Lang. Syst. 10(4), 513–554 (1988)

    Article  Google Scholar 

  5. Barden, R., Stepney, S., Cooper, D.: Z in Practice. BCS Practitioner Series. Prentice Hall, New York (1994)

    MATH  Google Scholar 

  6. Boiten, E.: Z unification tools in generic formaliser. Technical report 10-97, Computing Laboratory, University of Kent at Canterbury (1997)

    Google Scholar 

  7. Boiten, E., Derrick, J.: IO-refinement in Z. In: Evans, A., Duke, D., Clark T. (eds.) 3rd BCS-FACS Northern Formal Methods Workshop. Springer (1998). https://ewic.bcs.org/content/ConWebDoc/4354

  8. Boiten, E., Derrick, J., Bowman, H., Steen, M.: Consistency and refinement for partial specification in Z. In: Gaudel and Woodcock [20], pp. 287–306

    Google Scholar 

  9. Boiten, E.A.: Perspicuity and granularity in refinement. In: Proceedings 15th International Refinement Workshop, EPTCS, vol. 55, pp. 155–165 (2011)

    Google Scholar 

  10. Boiten, E.A.: Introducing extra operations in refinement. Form. Asp. Comput. 26(2), 305–317 (2014)

    Article  MathSciNet  Google Scholar 

  11. Boiten, E.A., Derrick, J.: From ODP viewpoint consistency to integrated formal methods. Comput. Stand. Interfaces 35(3), 269–276 (2013). https://doi.org/10.1016/j.csi.2011.10.015

    Article  Google Scholar 

  12. Boiten, E.A., Derrick, J., Schellhorn, G.: Relational concurrent refinement II: internal operations and outputs. Form. Asp. Comput. 21(1–2), 65–102 (2009). http://www.cs.kent.ac.uk/pubs/2007/2633

  13. Derrick, J., Boiten, E.: Refinement – Semantics, Languages and Applications. Springer, Berlin (2018)

    Book  Google Scholar 

  14. Derrick, J., Boiten, E., Bowman, H., Steen, M.: Viewpoints and consistency: translating LOTOS to Object-Z. Comput. Stand. Interfaces 21, 251–272 (1999)

    Article  Google Scholar 

  15. Derrick, J., Boiten, E.A.: Relational concurrent refinement. Form. Asp. Comput. 15(1), 182–214 (2003)

    Article  Google Scholar 

  16. Derrick, J., Boiten, E.A.: Refinement in Z and Object-Z, 2nd edn. Springer, London (2014). https://doi.org/10.1007/978-1-4471-0257-1

    Book  MATH  Google Scholar 

  17. Derrick, J., Boiten, E.A., Bowman, H., Steen, M.W.A.: Specifying and refining internal operations in Z. Form. Asp. Comput. 10, 125–159 (1998)

    Article  Google Scholar 

  18. Derrick, J., Bowman, H., Boiten, E., Steen, M.: Comparing LOTOS and Z refinement relations. In: FORTE/PSTV’96, pp. 501–516. Chapman & Hall, Kaiserslautern (1996)

    Google Scholar 

  19. Flynn, M., Hoverd, T., Brazier, D.: Formaliser – an interactive support tool for Z. In: Nicholls J.E. (ed.) Z User Workshop, pp. 128–141. Springer, London (1990)

    Google Scholar 

  20. Gaudel, M.C., Woodcock, J.C.P. (eds.): FME’96: Industrial Benefit of Formal Methods, Third International Symposium of Formal Methods Europe. Lecture Notes in Computer Science, vol. 1051. Springer (1996)

    Google Scholar 

  21. van Glabbeek, R.J.: The linear time - branching time spectrum I. The semantics of concrete sequential processes. In: Bergstra, J., Ponse, A., Smolka S. (eds.) Handbook of Process Algebra, pp. 3–99. North-Holland (2001)

    Google Scholar 

  22. He, J., Hoare, C.A.R., Sanders, J.W.: Data refinement refined. In: Robinet, B., Wilhelm R. (eds.) Proceedings of ESOP 86, Lecture Notes in Computer Science, vol. 213, pp. 187–196. Springer, Berlin (1986)

    Google Scholar 

  23. Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall, Englewood Cliffs (1998)

    MATH  Google Scholar 

  24. Leduc, G.: On the role of implementation relations in the design of distributed systems using LOTOS. Ph.D. thesis, University of Liège, Liège, Belgium (1991)

    Google Scholar 

  25. Schellhorn, G.: ASM refinement and generalizations of forward simulation in data refinement: a comparison. Theor. Comput. Sci. 336(2–3), 403–435 (2005). https://doi.org/10.1016/j.tcs.2004.11.013

    Article  MathSciNet  MATH  Google Scholar 

  26. Smith, G., Derrick, J.: Specification, refinement and verification of concurrent systems - an integration of Object-Z and CSP. Form. Methods Syst. Des. 18, 249–284 (2001)

    Article  Google Scholar 

  27. Spivey, J.M.: The Z Notation: A Reference Manual. International Series in Computer Science, 2nd edn. Prentice Hall, Upper Saddle River (1992)

    MATH  Google Scholar 

  28. Stepney, S., Cooper, D., Woodcock, J.: More powerful data refinement in Z. In: Bowen, J.P., Fett, A., Hinchey M.G. (eds.) ZUM’98: The Z Formal Specification Notation. Lecture Notes in Computer Science, vol. 1493, pp. 284–307. Springer, Berlin (1998)

    Google Scholar 

  29. Woodcock, J., Stepney, S., Cooper, D., Clark, J., Jacob, J.: The certification of the mondex electronic purse to ITSEC level E6. Form. Asp. Comput. 20(1), 5–19 (2008). https://doi.org/10.1007/s00165-007-0060-5

    Article  Google Scholar 

  30. Woodcock, J.C.P., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice Hall, New York (1996)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. De Montfort University, Leicester, LE1 9BH, UK

    Eerke Boiten

  2. University of Sheffield, Sheffield, S1 4DP, UK

    John Derrick

Authors
  1. Eerke Boiten
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. John Derrick
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to John Derrick .

Editor information

Editors and Affiliations

  1. Unconventional Computing Laboratory, University of the West of England, Bristol, UK

    Andrew Adamatzky

  2. Joint Quantum Centre, Durham University, Durham, UK

    Vivien Kendon

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Boiten, E., Derrick, J. (2020). Understanding, Explaining, and Deriving Refinement. In: Adamatzky, A., Kendon, V. (eds) From Astrophysics to Unconventional Computation. Emergence, Complexity and Computation, vol 35. Springer, Cham. https://doi.org/10.1007/978-3-030-15792-0_8

Download citation

Publish with us

Policies and ethics

Search

Navigation