Information Technology Reference

In-Depth Information

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)

Search WWH ::

Custom Search