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

design patterns. The novel thing in our way is that we model design patterns as a list
of “propositions”, instead of the conjunction of propositions. This can greatly simplify
our definitions in latter works. Once we can model design patterns in lists, we can
easily describe their composition by concatenating lists. This is the bases for latter
works. See Table 3 for details.
In section 4, we give a formal proof of the composition of Composite and Decora-
tor pattern. First, as the composition of design patterns are modeled as lists, the prob-
lem of verifying correctness of the composition can be tackled by verifying certain
properties of these lists. In this way, we successfully formalized the “faithful” princi-
ple as two theorems about “lists” in Coq. Then we devise a couple of customized
tactics to facilitate the proof of these theorems. Our tactics take lists (design patterns)
as parameters, thus applicable to all the patterns modeled in the correct way (as lists).
By using our tactics, we prove that the composition in our example satisfies the prop-
erties required by these theorems, which means it is a correct composition in the sense
that it is a faithful composition.
Section 5 is conclusion and future works.
To sum up, we have developed a new way of modeling design pattern (as a list of
proposition). Based on this model, we can describe their composition as concatenation
of lists and formalize properties of compositions as properties of lists, which are eas-
ier to operate and verify. In the case study of Composite and Decorator pattern com-
position, we have shown that the correctness of pattern based composition can be
verified with the assist of Coq. Also, by using our carefully designed tactics, the prov-
ing processes can be done with a high level of automation.
All the materials presented in this paper are implemented and compiled in Coq v8.1
and available at [14]. Coq [12] is an interactive theorem proving and program devel-
opment tool, which is widely used in program verification and theorem proving.
2 Related Works
The formalization of design patterns was widely studied [3][5][16], and the works that
study their composition are also immense [1][2][4][6][7][15]. [1] studied composition
in general, and [2] proposed the concept of 'faithfulness'. Their works can apply to
any domain, but in this paper, we only focus on the domain of Object Oriented De-
sign. In [5], the authors formulated basic entities and relations to model the basic
concepts in OOD, which is similar to our work, but [5] mainly devoted to graphical
representations of OOD to facilitate understanding of system design, and do not con-
sidered pattern based compositions. [4][6][15] studied pattern based composition, and
used First Order Logic and Temporal Logic of Action to describe design patterns'
structure and behavior respectively. Both of them chose the 'faithfulness' principle as
correctness criteria, and analyzed the conditions that a correct composition must sat-
isfy. But their proofs are informal and manual, which is based on observations and
experiences. We adapt Coq as the proof assistance in this paper, which makes our
proof formal and gained a high level of automation.