Information Technology Reference
In-Depth Information
Definition composite_pattern : DesignPattern :=
(* Define the interface for the Class component *)
Memberfun operation component
::Memberfun add component
::Memberfun remove component
::Memberfun getchild component
(* Define the interface for the Class composite *)
::Memberfun operation composite
::Memberfun add composite
::Memberfun remove composite
::Memberfun getchild composite
(* Class composite references instances of Class component *)
::Reference composite component
(* Method invocation *)
::Invocate composite operation component operation
(* Define the interface of Class leaf *)
::Memberfun operation leaf
(* Define parameters of each Method *)
::Argument add component
::Argument remove component
::Argument getchild int
(* Define the hierarchy of Class Inheritance *)
::Inherit leaf component
::Inherit composite component::nil.
Fig. 4. Definition of Composite pattern in Coq
In practice, when software designers want to compose these two patterns, depend-
ing on their experiences and intuitions, they may compose them as in Figure 6 (in
UML class diagram). In fact, this composition forms as a new pattern. We call it the
Composite_Decorator pattern. Its formal counterpart is in Figure 7.
However, we cannot rely on the experiences and intuitions of the designer, because
this work is laborious and error-prone. First, there are many statements in each pat-
tern, the designer may lose statements in the original patterns, or add undesirable new
statements in the composition. Additionally, as we can see in Figure 6, there is a
mapping between entities in the separate design patterns before the composition and
entities in after the composition, because some entities play roles in both separate
patterns, for example, the class “TheComponent”, the method “TheOperation”. There-
fore, we need to define functions to record all these information for the designer,
which serve as a base for the proof of correctness of pattern compositions. That is the
main job in the next section.
Search WWH ::

Custom Search