Information Technology Reference
In-Depth Information
Mcmp and Mdcr are maps defined based on CM and MM. For details of these defi-
nitions, see [14].
Beasd on these definitions, we now formalize the principle of faithfulness in Coq.
As mentioned in Section 1, the theorems are actually properties about lists, which is
easier to formulate and verify in Coq.
( t:term), In t (Composite\/Decorator)→
(s:term),In s Composite_Decorator/\(Mcmp_dcr t=s). (2)
( t:term), In t Composite_Decorator→
(s:term), In s (Composite
Decorator)/\(Mcmp_dcr s=t). (3)
Decorator) is not only the disjoint union of Composite and Decorator, it
is the deductive closure of their union. The closure is calculated by our function “Un-
ion” and “Closure” in Coq, see Figure 9 and 10 for details.
Usually, we allow some new facts to be deduced from the union of two patterns,
with explicitly specified rules. Otherwise, any other new facts would be undesirable,
and would be regarded as an error in the composition. As far as the structure is con-
cerned, we would like to define some larger building block in the OOD, for instance,
the polymorphism, which can be described by the elemental constructs in the induc-
tive type 'term'. Clearly, this related to a more sophisticated problem, that is: what
properties should remain after the composition. For simplicity, we just concern the
elemental statements in each pattern in this paper. However, to make our approach
more practical for everyday use, we should concern more complex properties in each
pattern. We leave it as our future work.
In our example, there is only one rule allowed for reasoning, that is:
Inherit a b, Inherit b c=> Inherit a c. (4)
(* Inductively calculate the Union of list l and m, which remove the same elements
in l and m *)
Fixpoint union (l m:list term) { struct l } : list term:=
match l with
(* if l is null, then return list m *)
| nil => m
(* if l is not null, check the number of occurrence of a in m *)
| a::l' =>
if Z_eq_dec (nb_occ a m) 0
(* if a does not occur in m, then add a to the resulting list *)
then a::union l' m
(* if a occur in m, then do not add a to the resulting list *)
else union l' m end.
Fig. 9. Definion of Union
Search WWH ::

Custom Search