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

3 Problem Illustration
In OOD, Class and Method are identified as basic entities, and a set of primary rela-
tions were formulated to model the basic concepts in OOD. The number and name of
these relations might differ from one another [4][5][6]. In our approach, we define the
following inductive type in Coq as in Figure 1.
(* Entities as Sets in Coq *)
Parameter Class : Set.
Parameter Method : Set.
Inductive term : Set :=
(* Class x inherit from Class y *)
| Inherit (x :Class) (y : Class) : term
(* Method m is a member function of Class c *)
| Memberfun (m:Method) (c:Class): term
(* Class x defines a member whose type is reference(s) to instance(s) of Class y *)
| Reference (x:Class)(y:Class):term
(* Method in Class c1invokes Method m2 in Class c2 *)
| Invoke(c1:Class)(m1:Method)(c2:Class) (m2:Method) : term
(*reference of Class c is an argument of Method m *).
| Argument (m:Method)(c:Class):term
Fig. 1. Inductive definition of term
Words in (* *) are comments. This definition serves as a grammar of writing speci-
fications about design patterns. Some authors [5] treat entities as unary relations.
However, we just define them as Sets in Coq. Treating them in this way gives us a
typed system, which improves readability and simplicity. As we can see from the
inductive definition of term, all the relations are typed, taking parameters from Class
and Method.
The clauses are actually the constructor of the Set term. It is easy to add new rela-
tions by adding new clauses in the inductive definition. Our definition of term is
flexible enough to add any relations that character the structure of design patterns.
Note we only focus on the structural aspect of design patterns in this paper. Though
our definition is general enough to model patterns in the structural category in [8], it
should be extended to model the behavioral aspect of design pattern. We leave it as
our future work, see Section 5 for details.
Usually, it will take many terms to precisely describe a design patter. So we model
design patterns as a list of 'terms':
Definition DesignPattern:= list term. (1)