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.
Full paper : PDF 241K
@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
)