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

Note in Figure 15, the tactic not_add_tac has done most of the job in the proof of
theorem (3). According to our definition of the not_add tac, the Coq system will
automatically search the right terms for the 'exists' statements in the goal. Howerver,
as we explicitly allow the deductive rule in formula (4), thus there are some extra
lines in the proof, which need to be handled manually and this is only a tiny part of
the whole proof.
Till now, we have demonstrated our formal way step by step, and have proven that
the example composition is a correct one. By following our way, designers can prove
the correctness of their own composition. Firstly, the designer should translate the
informal description of design patterns in UML to the formal description in Coq. This
task is laborious and we should develop some tools to automate this translation. Then,
as we can see, the definition of the type of mapping functions and the parameterized
tactics are general enough for the designer to reuse. The only information that de-
signer need to offer is the implementation of the mapping functions, as we did in the
examples in Figure 8, which are specific to the Composite and Decorator pattern.
After implementing the mapping functions, the way followed is rather straightfor-
ward. As we model design patterns as a list of 'terms', the formalization of the cor-
rectness criterion for designer's own patterns can be obtained by just replacing the
name of the lists occurred in formula (2) and (3). Finally, the proving process is rather
easy by passing the correct parameters to our customized tactics.
Once a composition is proven to be correct, it can be reused repeatedly in the process
of system construction. This would facilitate reuse of design in a larger scale and reduce
errors in design phase, which justifies all the efforts of verifying their correctness.
(*This tactic takes list l1.l2,M as parameters,which is more general than not_add_tac,
reader may redefine the not_add_tac to make it more general, however the optimiza-
tion of that tactic is not in the interest of this paper *)
Ltac not_lose_tac l1 l2 M:=
(* Match the current goal. If the conclusion in the current goal is of the form after |-,
then we can actually 'program' the proof according the values of parameters, i.e.,
l1,l2 and M. *)
match goal with
| [ |-forall t:term, In t l1 ->(exists s:term, In s l2/\M t=s) ]=>
( intro t ;
simpl;
intuition;
(* the term t is the term we need to find in l1. Usually this is done manually, however
our tactic help us find the right term in l1. *)
exists (M t);
subst; simpl; auto. )
end.
Fig. 13. Definition of the not_lose_tac tactic