Information Technology Reference
In-Depth Information
Particularly, as to our case study, this means: for the composition of Composite and
Decorator pattern to be correct, it must satisfy the following two conditions:
No statement in Composite and Decorator loses after the composition.
No new properties about Composite and Decorator can be added after the composition.
4.2 Formalizing the Correctness Criterion in Coq
Before formalizing the correctness criterion, we should define some mapping func-
tions between entities (Class and Method) before and after the composition. These
functions contain the key information of the composition. Now we explicitly define
these mapping functions in Figure 8.
(* Mapping from Class to Class *)
CM : Class -> Class
(* Mapping from Method to Method *)
MM :Method ->Method
(* Mapping from Composite to Composite_Decorator *)
Mcmp:Composite->Composite_Decorator
(* Mapping from Decorator to Composite Decorator *)
Mdcr:Decorator->Composite_Decorator
(* The whole Mapping relation is the combination of Mcmp and Mdcr *)
Mcmp_dcr := Mcmp \/ Mdcr.
(* Concrete mapping functions *)
(* Class mapping from Composite pattern to the composition *)
Definition ClsMcmp : Class -> Class := fun c:Class => match c with
| component=>thecomponent
| leaf =>leafconcretecomp
| composite =>compositedecorator
| others => others end.
(* Method mapping from Composite pattern to the composition *)
Definition MtdMcmp : Method -> Method := fun m => match m with
| operation => theoperation
| others => others end.
(* Class mapping from Decorator pattern to the composition *)
Definition ClsMdcr : Class -> Class :=fun c:Class=>match c with
| component => thecomponent
| concretecomponent => leafconcretecomp
| decorator => compositedecorator
| others => others end.
(* Method mapping from Decorator pattern to the composition *)
Definition MtdMdcr : Method -> Method :=fun m => match m with
| operation => theoperation
| others=> others end.
Fig. 8.
Mapping functions in Coq
Search WWH ::
Custom Search