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

Description and Verification of
Pattern-Based Composition in Coq *
Qiang Liu, Zhongyuan Ynag, and Jinkui Xie
Department of Computer Science and Technology, East China Normal University
Dongchuan Rd. 500, 200241 Shanghai, China
{lqiang,yzyuan,jkxie}@cs.ecnu.edu.cn
Abstract. Design patterns were treated as design components, which serve as
elemental components and can be composed to construct a large software sys-
tem. In the process of composition, the key problem is how to ensure the cor-
rectness of composition. In this paper, we use First Order Logic to model some
elemental entities and relations in Object Oriented Design, which serve as an
ontology in the domain. Then we use the vocabulary in the ontology to specify
design patterns and formalize the “faithful” principle as theorems in Coq. Fi-
nally, we prove these theorems and 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.
Keywords: Design patterns, Composition, Verification, Coq, Faithfulness.
1 Introduction
Design patterns [8] are widely used in modern software systems. In the Component-
Based approach, design patterns were treated as design components, which serve as
elemental components of Object Oriented Design (OOD) and can be composed to
construct a large software system. In the process of composition, the key problem is to
ensure the correctness of composition. This is a difficult and larger top, and far from
being resolved. In this paper, we set our discussion to the domain of the object ori-
ented design, and restrict our discussion in the composition of design patterns. This
paper is organized in the following way:
Section 2 introduces related works and comments are also available.
In Section 3, we illustrate the problem by a case study, the composition of Compos-
ite and Decorator pattern. In order to model design patterns in Coq, we use First Order
Logic to capture the basic entities (Class and Method) and relations in the domain of
OOD (Inherit etc). They are both modeled by Inductive types in Coq. These entities
and relations are the basic vocabularies based on which we can faithfully describe
* The research in this paper was supported by Research Fund for the Doctoral Program of
Higher Education of China, No. 20060269002.