Susan Stepney, Fiona Polack, Ian Toyn
Patterns to Guide Practical Refactoring: examples targetting promotion in Z.

In Didier Bert, Jonathan P. Bowen, Steve King, Marina Waldén, editors. ZB2003: Third International Conference of B and Z Users, Turku, Finland, June 2003 . LNCS 2651:20-39. Springer, 2003.

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.

@inproceedings(SS-ZB-03b,
  author = "Susan Stepney and Fiona Polack and Ian Toyn",
  title = "Patterns to Guide Practical Refactoring:
           examples targetting promotion in {Z}",
  pages = "20--39",
  crossref = "ZB-03"
)

@proceedings(ZB-03,
  title = "ZB2003: Third International Conference of B and Z Users,
                   Turku, Finland",
  booktitle = "ZB2003: Third International Conference of B and Z Users,
                   Turku, Finland",
  editor = "Didier Bert and Jonathan P. Bowen and Steve King and Marina Walden",
  series = "LNCS",
  volume = 2651,
  publisher = "Springer",
  year = 2003
)