Abstract
Formal methods such as Z are generally criticised for their lack of practical applicability. As in other areas of software engineering, patterns help to construct, analyse and describe formal texts. Once a method has a catalogue of patterns, development can proceed by applying patterns, and by moving from one sort of pattern to another. This paper illustrates a developmental use of patterns. First, we describe the set of patterns that collectively represent the well-known Z structure, promotion. We then show how refactoring can be used to take an unstructured Z specification in to a promotion structure.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Christopher Alexander, Sara Ishikawa, Murray Silverstein, Max Jacobson, Ingrid Fiksdahl-King, and Shlomo Angel. A Pattern Language: Towns, Buildings, Construction. Oxford University Press, 1977.
Rosalind Barden, Susan Stepney, and David Cooper. Z in Practice. BCS Practitioner Series. Prentice Hall, 1994.
Jonathan P. Bowen, Steve Dunne, Andy Galloway, and Steve King, editors. ZB2000: First International Conference of B and Z Users, volume 1878 of LNCS. Springer, 2000.
David Cooper and Susan Stepney. Segregation with communication. In [Bowen et al. 2000], pages 451–470.
Mark d’Inverno and Michael Luck. Understanding Agent Systems. Springer, 2001.
Martin Fowler. Refactoring: improving the design of existing code. Addison-Wesley, 1999.
Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides. Design Patterns. Addison-Wesley, 1995.
Carroll Morgan and Bernard Sufrin. Specification of the UNIX filing system. IEEE Trans. Softw. Eng, 10(2):128–142, 1984.
Susan Stepney and David Cooper. Formal methods for industrial products. In [Bowen et al. 2000], pages 374–393.
Susan Stepney, Rosalind Barden, and David Cooper, editors. Object Orientation in Z. Springer, 1992.
Susan Stepney, David Cooper, and Jim Woodcock. An electronic purse: Specification, refinement, and proof. Technical Monograph PRG-126, Programming Research Group, Oxford University Computing Laboratory, 2000.
Susan Stepney, Fiona Polack, and Ian Toyn. Refactoring in maintenance and development of Z specifications and proofs. In REFINE 2002, Copenhagen, volume 70(3) of ENTCS. Elsevier, 2002.
Susan Stepney, Fiona Polack, and Ian Toyn. An outline pattern language for Z. 2003. (these proceedings).
Susan Stepney, Fiona Polack, and Ian Toyn. A Z patterns catalogue I: specification and refactoring, v0.1. Technical Report YCS-2003-349, York, 2003.
J. C. P. Woodcock and J. Davies. Using Z: Specification, Refinement, and Proof. Prentice-Hall, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stepney, S., Polack, F., Toyn, I. (2003). Patterns to Guide Practical Refactoring: Examples Targetting Promotion in Z. In: Bert, D., Bowen, J.P., King, S., Waldén, M. (eds) ZB 2003: Formal Specification and Development in Z and B. ZB 2003. Lecture Notes in Computer Science, vol 2651. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44880-2_3
Download citation
DOI: https://doi.org/10.1007/3-540-44880-2_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40253-4
Online ISBN: 978-3-540-44880-8
eBook Packages: Springer Book Archive