FORMALISING DESIGN PATTERNS

This paper views design patterns [5] as a transformation from a “before” system consisting of a set of classes (often a single unstructured class) into an “after” system consisting of a collection of classes organised by the pattern. To prove that these transformations are formal refinements, we adopt a version of the Object Calculus [4] as a semantic framework. We make explicit the conditions under which these transformations are formally correct. We give some additional design pattern transformations which have been termed “annealing” in the VDM++ world, which include the introduction of concurrent execution into an initially sequential system. We show that these design patterns can be classified on the basis of a small set of fundamental transformations which are reflected in the techniques used in the proof of their correctness.