Abstract
Applying transformations to object-oriented systems usually affects source code and its associated models, involving complex maintenance efforts to keep those artifacts up to date. Most projects abandon design information in the form of models early in the life cycle, as their maintenance becomes extremely expensive. In this paper, we propose a complete catalog of object model laws (bidirectional semantics-preserving transformations) for Alloy, a formal object-oriented modeling language. We address relative completeness through a reduction process that transforms an arbitrary Alloy model into an equivalent model in a core language (normal form). We evaluate our completeness result using two distinct normal forms.
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
Massoni, T., Gheyi, R., Borba, P.: Formal model-driven program refactoring. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 362–376. Springer, Heidelberg (2008)
Gheyi, R.: A Refinement Theory for Alloy. PhD thesis, UFPE (2007)
Jackson, D.: Software Abstractions: Logic, Language and Analysis. MIT Press, Cambridge (2006)
Gheyi, R., Massoni, T., Borba, P.: Formally introducing alloy idioms. In: Brazilian Symposium on Formal Methods, Brazil, pp. 22–37 (2007)
Owre, S., et al.: PVS language reference (2007), http://pvs.csl.sri.com
Gheyi, R., Massoni, T., Borba, P.: A rigorous approach for proving model refactorings. In: 20th Automated Software Engineering Conference, pp. 372–375 (2005)
Gheyi, R., Massoni, T., Borba, P.: An abstract equivalence notion for object models. Electronic Notes in Theoretical Computer Science 130, 3–21 (2005)
Hoare, C., et al.: Laws of programming. CACM 30(8), 672–686 (1987)
Borba, P., et al.: Algebraic Reasoning for Object-Oriented Programming. Science of Computer Programming 52, 53–100 (2004)
Banerjee, J., et al.: Semantics and implementation of schema evolution in object-oriented databases. In: Int. Conf. on Management of Data, pp. 311–322 (1987)
Bergstein, P.: Object-preserving class transformations. In: OOPSLA, pp. 299–313 (1991)
Sunyé, G., et al.: Refactoring UML models. In: UML, pp. 134–148 (2001)
Gogolla, M., Richters, M.: Equivalence rules for UML class diagrams. In: UML, pp. 87–96 (1998)
Lano, K., Bicarregui, J.: Semantics and transformations for UML models. In: UML, pp. 97–106 (1998)
Evans, A.: Reasoning with UML class diagrams. In: 2nd IEEE Workshop on Industrial Strength Formal Specification Techniques, pp. 102–113 (1998)
McComb, T.: Refactoring Object-Z specifications. In: Wermelinger, M., Margaria-Steffen, T. (eds.) FASE 2004. LNCS, vol. 2984, pp. 69–83. Springer, Heidelberg (2004)
Frias, M., Pombo, C., Baum, G., Aguirre, N., Maibaum, T.: Reasoning about static and dynamic properties in alloy: A purely relational approach. ACM Transactions on Software Engineering Methodology 14(4), 478–526 (2005)
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
Gheyi, R., Massoni, T., Borba, P., Sampaio, A. (2009). A Complete Set of Object Modeling Laws for Alloy. In: Oliveira, M.V.M., Woodcock, J. (eds) Formal Methods: Foundations and Applications. SBMF 2009. Lecture Notes in Computer Science, vol 5902. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-10452-7_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-10452-7_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-10451-0
Online ISBN: 978-3-642-10452-7
eBook Packages: Computer ScienceComputer Science (R0)