Formalization Of Design Patterns And Its Implementation In EMF

Design Patterns, one of the most important concepts in software engineering, docu-ment frequently encountered problems in Object-Oriented Design(OOD) and provides software designers with elegant and reusable solutions which are easy to understand, maintain and extend. Due to this reason, patterns are widely used in modern software systems and have become critical means for communications between designers.However, huge ambiguities exist in understanding patterns, since traditional meth-ods of pattern specification are informal,e.g., semi-formal UML diagrams and annotated English in [98]. Furthermore, due to the lack of proper abstraction mechanism, essential pattern-related concepts could not be described in a proper way. Finally, with informal specifications, it is impossible to provide automatic tool support for design patterns.Meanwhile, a set of pattern-related problems are identified in pattern practices, e.g., Pattern Instantiation, Pattern Evolution and Pattern Implementation. To provide tool sup-port for these problems, pattern specifications should be formalized. Otherwise, designers who are supposed to focus on their business logic, have to handle these problems manu-ally, which is very inefficient and error-prone.Therefore, for the problem of pattern formalization, this paper conducted the follow-ing researches:·Adopt Theorem Prover Coq to formalize the structure of design patterns. During the process, this paper makes use of Coq’s Module System to define each pattern as an abstract Module Type which includes the pattern’s basic structure and structural specification.·While describing a pattern’s basic structure, Record Type is used and combined with polymorphic set to categorize pattern’s participants into singular participants and set participants. This distinction decouples solutions for pattern-related prob-lems and provides opportunities for introducing Aspect-Oriented Modeling(AOM) into the problem domain. Specifically, Pattern Instantiation could be solved by han-dling singular participants and Pattern Evolution by handling set participants.·Based on a pattern’s basic structure, this paper uses Coq’s higher-order logic to define a set of simple and complex relations to precisely capture various structural features of pattern’s participants. The resulting features form the foundations of a pattern’s structural specifications. ·By following the metamodeling approach, this paper implements the formal speci-fications in Coq and provides practical tool support for pattern’s applications in the industrial-level modeling framework Eclipse Modeling Framework(EMF).The basic structure and structural specifications constitute a pattern’s formal specifi-cation. Based on the specification, it is possible to formally study pattern-related problems and provide corresponding solutions. This paper studies three pattern-related problems: Pattern Instantiation, Pattern Evolution and Pattern Implementation. For each problem, this paper provides the following solutions:·For the problem of Pattern Instantiation, a instantiation function is defined to take structural variants of the pattern as parameters and return an instance in which sin-gular participants are properly assigned to satisfy the pattern specification. After-ward, the correctness theorem of the instantiation function is formulated using Co-q’s specification language and the proof of theorem is completed in the Coq Proof System.·To formalize the problem of Pattern Evolution in Coq, evolutionary rules are ab-stracted according to a pattern’s structural features and formulated as evolutionary functions. Each function returns an instance in which all its set participants are properly assigned in the sense that the pattern specification is still satisfied. Simi-larly, the correctness theorem of each evolutionary rules are formalized and proved in Coq.·For the problem of Pattern Implementation, this paper adopts basic concepts in the Situation Calculus(SC) to understand run-time pattern system as a dynamic system in SC and pattern-related actions as actions in SC. According to SC, the most im-portant function of actions is to change truth values of dynamic relations(Fluents). Consequently, to completely and precisely describe pattern’s behavioral features, this paper explicitly defines the concept of dynamic relations, which are totally im-plicit in traditional specifications.·For each pattern-related problem, this paper implements corresponding solutions in EMF. By integrating these solutions in a single framework, we actually have developed a prototype of a Pattern Management System.To sum up, this paper formally studied pattern specification and pattern-related prob-lems in Coq, and also implemented the corresponding concepts in EMF to provide prac-tical and efficient tool support for pattern-based software development.