Abstract
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. 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. Finally, 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.
The research in this paper was supported by Research Fund for the Doctoral Program of Higher Education of China, No. 20060269002.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Lamport, L.: Composing specifications. ACM Transactions on Programming Languages and Systems 15(1), 73–132 (1993)
Moriconi, M., Qian, X., Riemenschneider, R.A.: Correct architecture refinement. IEEE Transactions on Software Engineering 21(4), 356–372 (1995)
Tommi, M.: Formalizing design pattern. In: Proceedings of the 20th International Conference on Software Engineering, pp. 115–124 (1998)
Taibi, T., Ngo, D.C.L.: Formal specification of design pattern combination using BPSL. International Journal of Information and Software Technology (IST) 45(3), 157–170 (2003)
Eden, A.H., Hirshfeld, Y.: Principles in formal specification of object-oriented architectures. In: Proceedings of the 11th CASCON, Toronto, Canada (November 2001)
Dong, J., Alencar, P., Cowan, D.: Ensuring structure and behavior correctness in design composition. In: Proceedings of the 7th Annual IEEE International Conference and Workshop on Engineering of Computer Based Systems (ECBS), Edinburgh UK, pp. 279–287 (2000)
Keller, R., Reinhard, S.: Design components: towards software composition at the design level. In: Proceedings of the 20th International Conference on Software Engineering, pp. 302–311 (1998)
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns, Elements of Reusable Object-Oriented Software. Addison-Wesley Publishing Company, Reading (1995)
Lamport, L.: The temporal logic of actions. ACM Transactions on Programming Languages and Systems 16(3), 873–923 (1994)
Coquand, T., Huet, G.: The calculus of constructions.Technical Report 530, INRIA (1986)
Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol. 7. Cambridge University Press, Cambridge (1989)
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. In: Texts in Theoretical Computer Science. Springer, Heidelberg (2004)
Alencar, P., Cowan, D., Lucena, C.: A formal approach to architectural design patterns. In: Gaudel, M.-C., Woodcock, J.C.P. (eds.) FME 1996. LNCS, vol. 1051, pp. 576–594. Springer, Heidelberg (1996)
Pattern Composition in Coq, http://ecnucs-selab.googlecode.com/files/exampleinpaper
Dong, J., Alencar, P.S.C., Cowan, D.D., Yang, S.: Composingpattern-based components and verifying correctness. The Journal of Systems and Software, 1755–1769 (2007)
Eden, A.H., Hirshfeld, Y., Kazman, R.: Abstraction classes in software design. IEE Software 153(4), 163–182 (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Liu, Q., Ynag, Z., Xie, J. (2009). Description and Verification of Pattern-Based Composition in Coq. In: Kim, Th., et al. Advances in Computational Science and Engineering. FGCN 2008. Communications in Computer and Information Science, vol 28. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-10238-7_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-10238-7_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-10237-0
Online ISBN: 978-3-642-10238-7
eBook Packages: Computer ScienceComputer Science (R0)