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 )