×

A static semantics for Alloy and its impact in refactorings. (English) Zbl 1279.68185

Sampaio, Augusto (ed.), Proceedings of the second Brazilian symposium on formal methods (SBMF 2005), Porto Alegre, RS, Brazil, November 30, 2005. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 184, 209-233 (2007).
Summary: Refactorings are usually proposed in an ad hoc way because it is difficult to prove that they are sound with respect to a formal semantics, not guaranteeing the absence of type errors or semantic changes. Consequently, developers using refactoring tools must rely on compilation and tests to ensure type-correctness and semantics preservation, respectively, which may not be satisfactory to critical software development. In this paper, we formalize a static semantics for Alloy, which is a formal object-oriented modeling language, and encode it in prototype verification system (PVS). The static semantics’ formalization can be useful for specifying and proving that transformations in general (not only refactorings) do not introduce type errors, for instance, as we show here.
For the entire collection see [Zbl 1275.68031].

MSC:

68Q55 Semantics in the theory of computing
68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Ambler, S.; Sadalage, P., Refactoring Databases: Evolutionary Database Design (2006), Addison-Wesley
[2] Banerjee, J.; Kim, W.; Kim, H.-J.; Korth, H., Semantics and implementation of schema evolution in object-oriented databases, (SIGMOD ’87: Proceedings of the 1987 ACM SIGMOD international conference on Management of data (1987), ACM Press: ACM Press New York, NY, USA), 311-322
[3] Bergstein, P., Object-preserving class transformations, (OOPSLA ’91: Conference proceedings on Object-oriented programming systems, languages, and applications (1991), ACM Press: ACM Press New York, NY, USA), 299-313
[4] Bergstein, P. (1994). Managing the Evolution of Object-oriented Systems; Bergstein, P. (1994). Managing the Evolution of Object-oriented Systems
[5] Borba, P.; Sampaio, A.; Cavalcanti, A.; Cornélio, M., Algebraic Reasoning for Object-Oriented Programming, Science of Computer Programming, 52, 53-100 (2004) · Zbl 1091.68027
[6] Eclipse project (2006), At
[7] Edwards, J., Jackson, D., and Torlak, E. (2004). A type system for object models. In 12th Foundations of software engineering; Edwards, J., Jackson, D., and Torlak, E. (2004). A type system for object models. In 12th Foundations of software engineering
[8] Evans, A. (1998). Reasoning with UML class diagrams. In 2nd IEEE Workshop on Industrial Strength Formal Specification Techniques; Evans, A. (1998). Reasoning with UML class diagrams. In 2nd IEEE Workshop on Industrial Strength Formal Specification Techniques
[9] Fowler, M., Refactoring: Improving the Design of Existing Code (1999), Addison-Wesley · Zbl 1020.68632
[10] Frias, M., Fork Algebras in Algebra, Logic and Computer Science (2002), World Scientific Publishing Co. · Zbl 1012.03001
[11] Frias, M.; Galeotti, J.; Pombo, C.; Aguirre, N., Dynalloy: Upgrading alloy with actions, (27th International Conference on Software Engineering (2005), ACM Press), 442-451
[12] Frias, M.; Pombo, C.; Aguirre, N., An equational calculus for alloy, (6th International Conference on Formal Engineering Methods. 6th International Conference on Formal Engineering Methods, Lecture Notes in Computer Science (2004), Springer-Verlag), 162-175
[13] 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)
[14] Gheyi, R., Massoni, T., and Borba, P. (2004). Basic Laws of Object Modeling. In 3rd Specification and Verification of Component-Based Systems, affiliated with ACM SIGSOFT 2004/FSE-12; Gheyi, R., Massoni, T., and Borba, P. (2004). Basic Laws of Object Modeling. In 3rd Specification and Verification of Component-Based Systems, affiliated with ACM SIGSOFT 2004/FSE-12
[15] Gheyi, R., Massoni, T., and Borba, P. (2005a). A Rigorous Approach for Proving Model Refactorings. In 20th IEEE/ACM International Conference on Automated Software Engineering (ASE); Gheyi, R., Massoni, T., and Borba, P. (2005a). A Rigorous Approach for Proving Model Refactorings. In 20th IEEE/ACM International Conference on Automated Software Engineering (ASE) · Zbl 1272.68248
[16] Gheyi, R.; Massoni, T.; Borba, P., An Abstract Equivalence Notion for Object Models, Elsevier’s Electronic Notes in Theoretical Computer Science, 130, 3-21 (2005) · Zbl 1272.68248
[17] Gogolla, M. and Richters, M. (1998). Equivalence rules for UML class diagrams. In The Unified Modeling Language, UML’98 - Beyond the Notation. First International Workshop, Mulhouse, France; Gogolla, M. and Richters, M. (1998). Equivalence rules for UML class diagrams. In The Unified Modeling Language, UML’98 - Beyond the Notation. First International Workshop, Mulhouse, France
[18] Jackson, D., Alloy: a lightweight object modeling notation, ACM Transactions on Software Engineering and Methodology, 11, 2, 256-290 (2002)
[19] Jackson, D., Software Abstractions: Logic, Language and Analysis (2006), MIT press
[20] Jackson, D.; Schechter, I.; Shlyahter, H., Alcoa: the alloy constraint analyzer, (22nd International Conference on Software Engineering (2000), ACM Press), 730-733
[21] Kleppe, A.; Warmer, J., The Object Constraint Language: Precise Modeling with UML (1999), Addison-Wesley
[22] Kleppe, A.; Warmer, J.; Bast, W., MDA Explained (2003), Addison-Wesley
[23] Lano, K. and Bicarregui, J. (1998). Semantics and transformations for UML models. In 1st Unified Modeling Language; Lano, K. and Bicarregui, J. (1998). Semantics and transformations for UML models. In 1st Unified Modeling Language · Zbl 0991.68039
[24] Lerner, B.; Habermann, A., Beyond schema evolution to database reorganization, (OOPSLA/ECOOP ’90: Proceedings of the European conference on object-oriented programming on Object-oriented programming systems, languages, and applications (1990), ACM Press: ACM Press New York, NY, USA), 67-76
[25] Liskov, B.; Guttag, J., Program Development in Java (2001), Addison-Wesley
[26] Marković, S.; Baar, T., Refactoring OCL annotated UML class diagrams, (Model Driven Engineering Languages and Systems, 8th International Conference, MoDELS. Model Driven Engineering Languages and Systems, 8th International Conference, MoDELS, LNCS, volume 3713 (2005), Springer-Verlag), 280-294
[27] McComb, T., Refactoring object-z specifications, (Fundamental Approaches to Software Engineering. Fundamental Approaches to Software Engineering, (FASE’04). Fundamental Approaches to Software Engineering. Fundamental Approaches to Software Engineering, (FASE’04), LNCS (2004), Springer-Verlag), 69-83 · Zbl 1129.68415
[28] Owre, S.; Rushby, J.; Shankar, N.; Stringer-Calvert, D., PVS Language Reference (2006), At
[29] Owre, S.; Rushby, J.; Shankar, N.; Stringer-Calvert, D., PVS prover guide (2006), At
[30] Penney, D.; Stein, J., Class modification in the gemstone object-oriented dbms, (OOPSLA ’87: Conference proceedings on Object-oriented programming systems, languages and applications (1987), ACM Press: ACM Press New York, NY, USA), 111-117
[31] Schürr, A. (2001). New type checking rules for OCL expressions. In Modellierung 2001, Workshop der Gesellschaft für Informatik e. V.; Schürr, A. (2001). New type checking rules for OCL expressions. In Modellierung 2001, Workshop der Gesellschaft für Informatik e. V.
[32] Skarra, A.; Zdonik, S., The management of changing types in an object-oriented database, (OOPSLA ’86: Conference proceedings on Object-oriented programming systems, languages and applications (1986), ACM Press: ACM Press New York, NY, USA), 483-495
[33] Sunyé, G.; Pollet, D.; Traon, Y.; Jézéquel, J.-M., Refactoring UML models, (4th Unified Modeling Language. 4th Unified Modeling Language, LNCS, volume 2185 (2001), Springer-Verlag), 134-148 · Zbl 1024.68864
[34] Tip, F.; Kiezun, A.; Baumer, D., Refactoring for Generalization Using Type Constraints, (18th Object-oriented programing, systems, languages, and applications (2003), ACM Press), 13-26
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.