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

Definition composite_decorator_composition: DesignPattern :=
(* Define the interface of Class thecomponent *)
Memberfun theoperation thecomponent
::Memberfun add thecomponent
::Memberfun remove thecomponent
::Memberfun getchild thecomponent
(* Define the interface of Class leafconcretecomp *)
::Memberfun theoperation leafconcretecomp
(* Define the interface of Class compositedecorator *)
::Memberfun theoperation compositedecorator
::Memberfun add compositedecorator
::Memberfun remove compositedecorator
::Memberfun getchild compositedecorator
(* References in this pattern *)
::Reference compositedecorator thecomponent
::Reference concretedecoratora addedstate
(* Define the interface of concrete decorators *)
::Memberfun theoperation concretedecoratora
::Memberfun theoperation concretedecoratorb
::Memberfun addedbehavior concretedecoratorb
(* Method invocation in this pattern *)
:: Invocate concretedecoratorb theoperation decorator operation
::Invocate concretedecoratorb theoperation concretedecoratorb addedbehavior
(* Arguments of each method *)
::Argument add thecomponent
::Argument remove thecomponent
::Argument getchild int
(* Define the hierarchy of Class Inheritance *)
::Inherit leafconcretecomp thecomponent
::Inherit compositedecorator thecomponent
::Inherit concretedecoratora compositedecorator
::Inherit concretedecoratorb compositedecorator::nil.
Fig. 7. Definition of composition of Composite and Decorator in Coq
we finished the proofs of the theorems formalized in Section 4.2 and defined two
customized tactics to allow some automation in the proving processes.
4.1 The Correctness Criterion
To prove the correctness of composition, we first need a correctness criterion. We
choose the well known principle of 'faithfulness' as our correctness criterion. In gen-
eral, for a composition to be faithful, it must satisfy the follow two conditions:
No component loses any properties after composition.
No new properties about each component can be added after composition.