Information Technology Reference
In-Depth Information
(*This theorem shows that for any desired property (term) of the compos-
ite_docorator, there is a correspondence in the composite_decorator', that is no prop-
erties are lost. *)
Theorem not_lose_Mcmp_dcr :
forall(t:term), Int composite_decorator ->
(existss:term, In s composite_decorator'/\Mcmp_dcr t=s).
Proof.
(*Pass the composite_decorator, composite_decorator' and Mcmp_dcr to tactic. *)
not_lose_tac composite_decorator composite_decorator' Mcmp_dcr.
Qed.
Fig. 14. The proof of the theorem not_lose_Mcmp_dcr
(*This theorem shows that for any properties in the composition, there is a corre-
spondence in the original patterns, that is, no undesirable properties are added. *)
Theorem not_add_Mcmp_dcr : forall (t:term), In t composite_decorator' ->
(exists s:term, In s composite_decorator/\Mcmp_dcr s=t).
Proof.
not_add_tac composite_decorator' composite_decorator.
exists (Inherit concretedecoratora component). auto .
exists (Inherit concretedecoratorb component ).auto.
Qed.
Fig. 15. The proof of the theorem not_add_Mcmp_dcr
5 Conclusions and Future Work
The main contribution of this paper is introducing a new approach for the formal
verification of pattern-based composition in Coq. We model the OOD in an inductive
type 'term' with several elemental constructs which capture basic concepts in the
domain of OOD. Then we defined some mapping functions and customized tactics to
facilitate the proving process. By using our basic definitions, designers can conven-
iently formulate desirable properties of design patterns as theorems in Coq and then
prove their correctness. Once a composition is proven to be correct, it can be reused
without any further proofs. This will facilitate reuse in a larger scale (not only reuse
of design pattern, but also their composition), which can benefit many aspects in the
developing process, including developing efficiency (using larger building blocks)
and reduce errors in design phase (the composition is proven to be correct). Addition-
ally, the composition is a larger logic unit (like the Composite_Decorator pattern),
which makes the system design easier to understand and maintain.
However, in this paper, our work is rather primitive. We only focus on the struc-
tural aspect of design patterns. As we all know, design patterns have both structure
and behavior. Though for some patterns it is enough to focus on their structural as-
pects, some design patterns do have behavioral significance, like Observer pattern. As
we can see, the elemental constructs in the definition of 'term' are all about Class and
Search WWH ::




Custom Search