earticle

영어

Design patterns capture elegant design solutions and facilitate reuse in design level. In the Component Based Software Engineering (CBSE), design patterns were treated as design components, which serve as elemental components and can be composed to construct a large software system. In the process of composition, the key problem is how to ensure the correctness of composition. To address this problem, a criterion for correct composition is needed. The well known “faithfulness” principle is chosen as the correctness criterion and our discussions are based on this principle. In this paper, we at first use First Order Logic to model some elemental entities and relations in Object Oriented Design, which serve as an ontology in the domain. Then using the vocabulary in the ontology, we formally specify design patterns and formalize the “faithful” principle as theorems in Coq. Finally, we prove the theorems and thus show the correctness of composition. As a case study, we described and verified the composition of Composite pattern and Decorator pattern. Once a composition is proven to be correct, one can use the composition repeatedly. 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.