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. Design patterns are characteristic structures of classes or objects which can be reused to achieve particular design goals in an elegant manner. For example, the "State" design pattern discussed in Section 5.1 below, replaces local attributes of a class that record its state (in the sense of a finite state machine) by an object which provides polymorphic functionality in place of conditionals depending upon the state. If design patterns are to be used for formal object-oriented languages and methods, such as VDM ++ [2], the conditions under which their use leads to a functionally-correct refinement step need to be identified. The semantics of object-oriented systems has been given in a logical axiomatic framework termed the Object Calculus [4] . Here, we use an extension of this framework which allows the use of structured actions corresponding to programming language statements, in order to formulate the semantics of the "before" and "after" versions of a system to which a design pattern has been applied, and show that the "after" version refines the "before" version. Section 2 introduces the object calculus and the syntax of VDM ++ [2] which we will use to illustrate design patterns. Sections 3, 4 and 5 consider some typical patterns from [5] and other sources, addressing creational patterns, structural patterns and behavioral patterns respectively. Section 6 gives a classification of design patterns and proof techniques. An object calculus [4] theory consists of collections of type and constant symbols, attribute symbols (denoting timevarying data), action symbols (denoting atomic operations) and a set of axioms describing the types of the attributes and the effects, permission constraints and other dynamic properties of the actions. The axioms are specified using linear temporal logic operators: (in the next state), u (in the previous state), U (strong until), S (strong since), 2 (always BCS-FACS Northern Formal Methods Workshop, 1996 FORMALISING DESIGN PATTERNS in the future) and (sometime in the future). There is assumed to be a first moment. The predicate BEG is true exactly at this time point. and u are also expression constructors. If e is an expression, e denotes the value of e in the next time interval, whilst u e denotes the value of e in the previous time interval. The version used here is that defined in [7] in order to give a semantics to VDM ++ . In this version actions are potentially durative and overlapping, with associated times !(; i), "(; i) and #(; i) denoting respectively the times at which the i-th invocation of is requested, activates and terminates (where i 2 N 1 ). Modal operators } "holds at a time" and~"value at a time" are added: '}t asserts that ' holds at t, whilst e~t is the value of e at time t. In order to give a semantics to a class C, in, for example, OMT [11], Syntropy [1] or VDM ++ , we define a theory C which has the type symbol @C representing all possible instances of C, attribute symbol C representing all the existing objects of C, and creation action new C (c : @C) and deletion action kill C (c : @C) which respectively add and remove c from this set. Each attribute att of objects c of C is formally represented by an attribute att(c : @C) of C (written as c:att for conformance with standard OO notation) and each method act(x : X) is represented by an action symbol act(c : @C; x : X), written as c!act(x). Output parameters and local variables of methods are also represented as attribute symbols. An additional attribute now is included to represent the current global time. Notice that C and now are class attributes and new C and kill C are class actions, whilst the c:att and c!act are at the object level. We can define the effect of methods by means of the "calling" operator between actions: 8 i : N 1 now = "(; i) ) 9 j : N 1 " ( ;j) = " ( ; i)# ( ;j) = # ( ; i) In other words: every invocation interval of is also one of . This generalises the Object Calculus formula ) to take account of the case where both actions are durative, and where may be composite. Composite actions are defined to represent specification statements and executable code: pre G post P names an action with the following properties: 8 i : N 1 now = "(; i) ) G}"(; i) 8 i : N 1 now = "(; i) ) P[att~"(; i)= ( att]}#(; i) In other words, G must be true at each activation time of , whilst P, with each "hooked" attribute ( att interpreted as the value att~"(; i) of att at initiation of , holds at the corresponding termination time. A frame axiom, termed the locality assumption, asserts that attributes of an object a of C can only be changed over intervals in which at least one of the actions a!m(e) of a executes [3]. Likewise, C can only change as a result of new C or kill C invocations. Assignment t 1 := t 2 can be defined as the action pre true post t 1 = ( t 2 where t 1 is an attribute symbol. Similarly sequential composition ";" and parallel composition "jj" of actions can be expressed as derived combinators:
In REF , various design patterns are formally proved to be refinement transformations in a semantical sense when compared to a more native/hard-wired encoding of the corresponding design pattern.
Formalising design patterns
FME 1996
Computer Science