Description and Verification of Pattern-Based Composition in Coq - Advances in Computational Science and Engineering - page 234

Fig. 2. Composite pattern in UML
Fig. 3. Decorator pattern in UML
The benefit of this definition is fully discussed in Section 1. Now, as a case study,
consider the composition of Composite pattern and Decorator pattern. Their descrip-
tions in UML class diagram are presented in Figure 2 and 3.
By the definition in Figure 1 and Formula (1), we can formally define Composite
pattern and Decorator pattern by using a list of 'terms' as in Figure 4 and 5. Figure 4
defines the participants in Composite pattern one by one. Note in the definition of
Reference relation, we do not explicitly state the name of the instance of Class com-
ponent and its cardinality. The reason for this is that our way is based on Class and
Method, we do not want to include the Object into our model, which is related to the
behavior of design patterns. As one can expected, in the definition of the Invocate
relation, we also omit the information related to Object and only specify the Type of
the Object, i.e., the Class. However, as in [5], this can be handled by introducing more
relations between Class and Method, or even between the sets of them. This is not a
problem for our model, because, as mentioned above, we can easily introduce new
relations by adding new clauses to the inductive definition of 'term'. However, the
focus in our paper is not to complete the set of relations, rather, we focus on introduc-
ing the approach of verifying pattern-based composition in Coq.