Stepney, Susan; Polack, Fiona; Toyn, Ian Patterns to guide practical refactoring: Examples targetting promotion in Z. (English) Zbl 1028.68555 Bert, Didier (ed.) et al., ZB 2003: Formal specification and development in Z and B. Third international conference of B and Z users, Turku, Finland, June 4-6, 2003. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2651, 20-39 (2003). Summary: 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.For the entire collection see [Zbl 1020.00016]. Cited in 1 Document MSC: 68Q60 Specification and verification (program logics, model checking, etc.) 68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) Keywords:Z; patterns; refactoring; development methods PDFBibTeX XMLCite \textit{S. Stepney} et al., Lect. Notes Comput. Sci. 2651, 20--39 (2003; Zbl 1028.68555) Full Text: Link