×

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].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
PDFBibTeX XMLCite
Full Text: Link