{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,30]],"date-time":"2026-09-30T18:02:17Z","timestamp":1790791337634,"version":"4.1.0"},"reference-count":100,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2023,4,5]],"date-time":"2023-04-05T00:00:00Z","timestamp":1680652800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100004919","name":"King Abdulaziz City for Science and Technology","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100004919","id-type":"DOI","asserted-by":"crossref"}]},{"name":"NSF","award":["1212683"],"award-info":[{"award-number":["1212683"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2023,4,30]]},"abstract":"<jats:p>\n            <jats:italic>Model Driven Engineering<\/jats:italic>\n            <jats:italic>(<\/jats:italic>\n            <jats:italic>\n              <jats:sans-serif>MDE<\/jats:sans-serif>\n            <\/jats:italic>\n            <jats:italic>)<\/jats:italic>\n            is a general-purpose engineering methodology to elevate system design, maintenance, and analysis to corresponding activities on models. Models (graphical and\/or textual) of a target application are automatically transformed into source code, performance models, Promela files (for model checking), and so on for system analysis and construction.\n          <\/jats:p>\n          <jats:p>\n            Models are instances of\n            <jats:italic>metamodels<\/jats:italic>\n            . One form an\n            <jats:sans-serif>MDE<\/jats:sans-serif>\n            metamodel can take is a [class diagram, constraints] pair: the class diagram defines all object diagrams that could be metamodel instances; object constraint language (\n            <jats:sans-serif>OCL<\/jats:sans-serif>\n            ) constraints eliminate semantically undesirable instances.\n          <\/jats:p>\n          <jats:p>\n            A metamodel\n            <jats:italic>refactoring<\/jats:italic>\n            is an invertible semantics-preserving co-transformation, i.e., it transforms both a metamodel\n            <jats:italic>and<\/jats:italic>\n            its models without losing data. This article addresses a subproblem of metamodel refactoring: how to prove the correctness of refactorings of class diagrams without\n            <jats:sans-serif>OCL<\/jats:sans-serif>\n            constraints using the\n            <jats:sans-serif>Coq<\/jats:sans-serif>\n            Proof Assistant.\n          <\/jats:p>","DOI":"10.1145\/3549541","type":"journal-article","created":{"date-parts":[[2022,7,26]],"date-time":"2022-07-26T11:11:16Z","timestamp":1658833876000},"page":"1-42","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["On Proving the Correctness of Refactoring Class Diagrams of MDE Metamodels"],"prefix":"10.1145","volume":"32","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9314-8116","authenticated-orcid":false,"given":"Najd","family":"Altoyan","sequence":"first","affiliation":[{"name":"The University of Texas at Austin, Austin, Texas, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8739-3841","authenticated-orcid":false,"given":"Don","family":"Batory","sequence":"additional","affiliation":[{"name":"The University of Texas at Austin, Austin, Texas, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,4,5]]},"reference":[{"key":"e_1_3_4_2_2","article-title":"Families to Persons: A Simple Illustration of Model-to-Model Transformation","author":"Allilaire F.","year":"2007","unstructured":"F. Allilaire and F. Jouault . 2007. Families to Persons: A Simple Illustration of Model-to-Model Transformation. https:\/\/www.eclipse.org\/atl\/documentation\/old\/ATLUseCase_Families2Persons.pdf.","journal-title":"https:\/\/www.eclipse.org\/atl\/documentation\/old\/ATLUseCase_Families2Persons.pdf"},{"key":"e_1_3_4_3_2","volume-title":"MDE Refactorings: A Categorical Framework with Proofs, Tools, and Implementations","author":"Altoyan N.","year":"2020","unstructured":"N. Altoyan . 2020. MDE Refactorings: A Categorical Framework with Proofs, Tools, and Implementations . Ph.D. Dissertation. University of Texas at Austin."},{"key":"e_1_3_4_4_2","article-title":"Coq Proof Scripts for Metamodel Co-Refactings","author":"Altoyan N.","year":"2022","unstructured":"N. Altoyan . 2022. Coq Proof Scripts for Metamodel Co-Refactings. https:\/\/zenodo.org\/record\/6645716#.YqoHOnb MKUl.","journal-title":"https:\/\/zenodo.org\/record\/6645716#.YqoHOnb MKUl"},{"key":"e_1_3_4_5_2","volume-title":"MoDeVVa","author":"Anastasakis K.","year":"2007","unstructured":"K. Anastasakis , B. Bordbar , and J. K\u00fcster . 2007. Analysis of model transformations via alloy. In MoDeVVa ."},{"key":"e_1_3_4_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30982-3_2"},{"key":"e_1_3_4_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90038-X"},{"key":"e_1_3_4_8_2","volume-title":"PSI","author":"Baar T.","year":"2007","unstructured":"T. Baar and S. Markovi\u0107 . 2007. A graphical approach to prove the semantic preservation of UML\/OCL refactoring rules. In PSI ."},{"key":"e_1_3_4_9_2","volume-title":"Automated Software Design Volume 1","author":"Batory D.","year":"2020","unstructured":"D. Batory . 2020. Automated Software Design Volume 1 (2nd ed.). Lulu.com."},{"key":"e_1_3_4_10_2","article-title":"Conversation About Theorem Proving with Warren Hunt","author":"Batory D.","year":"2021","unstructured":"D. Batory . 2021. Conversation About Theorem Proving with Warren Hunt. Private communication.","journal-title":"Private communication"},{"key":"e_1_3_4_11_2","volume-title":"MODELSWARD","author":"Batory D.","year":"2020","unstructured":"D. Batory and N. Altoyan . 2020. Aocl: A pure-java constraint and transformation langauge for MDE. In MODELSWARD ."},{"key":"e_1_3_4_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-015-0488-7"},{"issue":"12","key":"e_1_3_4_13_2","article-title":"Modularizing theorems for software product lines: The JBook case study","volume":"14","author":"Batory D.","year":"2008","unstructured":"D. Batory and E. B\u00f6rger . 2008. Modularizing theorems for software product lines: The JBook case study. Journal of Universal Computer Science 14, 12 (June2008), 2059\u20132082.","journal-title":"Journal of Universal Computer Science"},{"key":"e_1_3_4_14_2","volume-title":"MODELS","author":"Batory D.","year":"2013","unstructured":"D. Batory , E. Latimer , and M. Azanza . 2013. Teaching model driven engineering from a relational database perspective. In MODELS ."},{"key":"e_1_3_4_15_2","doi-asserted-by":"publisher","DOI":"10.5555\/1076267"},{"key":"e_1_3_4_16_2","volume-title":"ESOP","author":"Benzaken V.","year":"2014","unstructured":"V. Benzaken , \u00c9. Contejean , and S. Dumbrava . 2014. A Coq formalization of the relational data model. In ESOP ."},{"key":"e_1_3_4_17_2","article-title":"Generic Metamodel Refactoring with Automatic Detection of Applicability and Co-Evolution of Artefacts","author":"Berg H.","year":"2017","unstructured":"H. Berg and I. Yuh . 2017. Generic Metamodel Refactoring with Automatic Detection of Applicability and Co-Evolution of Artefacts. https:\/\/www.duo.uio.no\/handle\/10852\/54485?locale-attribute=no.","journal-title":"https:\/\/www.duo.uio.no\/handle\/10852\/54485?locale-attribute=no"},{"key":"e_1_3_4_18_2","doi-asserted-by":"publisher","DOI":"10.4064\/-28-1-167-190"},{"key":"e_1_3_4_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00778-007-0059-9"},{"key":"e_1_3_4_20_2","volume-title":"ACM SIGMOD","author":"Bernstein P.","year":"2007","unstructured":"P. Bernstein and S. Melnik . 2007. Model management 2.0: Manipulating richer mappings. In ACM SIGMOD ."},{"key":"e_1_3_4_21_2","volume-title":"NTIC","author":"Berramla K.","year":"2015","unstructured":"K. Berramla , E. Deba , and M. Senouci . 2015. Formal validation of model transformation with Coq proof assistant. In NTIC ."},{"key":"e_1_3_4_22_2","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: the Calculus of Inductive Constructions","author":"Bertot Y.","year":"2013","unstructured":"Y. Bertot and P. Cast\u00e9ran . 2013. Interactive Theorem Proving and Program Development: Coq\u2019Art: the Calculus of Inductive Constructions . Springer Science & Business Media."},{"key":"e_1_3_4_23_2","volume-title":"GTTSE","author":"B\u00e9zivin J.","year":"2006","unstructured":"J. B\u00e9zivin . 2006. Model driven engineering: An emerging technical space. In GTTSE , R. L\u00e4mmel , J. Saraiva , and J. Visser (Eds.). Springer, Berlin."},{"key":"e_1_3_4_24_2","doi-asserted-by":"publisher","DOI":"10.5555\/3103551"},{"key":"e_1_3_4_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.05.001"},{"key":"e_1_3_4_26_2","volume-title":"SBMF","author":"Calegari D.","year":"2011","unstructured":"D. Calegari , C. Lunas , N. Szasz , and \u00c1. Tasistro . 2011. A type-theoretic framework for certified model transformations. In SBMF ."},{"key":"e_1_3_4_27_2","volume-title":"SEKE","author":"Costa V.","year":"2014","unstructured":"V. Costa , R. Monteiro , and L. Murtao . 2014. Detecting semantic equivalence in UML class diagrams. In SEKE ."},{"key":"e_1_3_4_28_2","volume-title":"Relational Algebra and Equational Proofs","author":"de Kogel E.","year":"1993","unstructured":"E. de Kogel . 1993. Relational Algebra and Equational Proofs . Technical Report 93\/23. Eindhoven University of Technology."},{"key":"e_1_3_4_29_2","volume-title":"OOPSLA\/SPLASH","author":"Delaware B.","year":"2011","unstructured":"B. Delaware , W. Cook , and D. Batory . 2011. Theorem proving for product lines. In OOPSLA\/SPLASH ."},{"key":"e_1_3_4_30_2","volume-title":"FASE","author":"Ehrig H.","year":"2007","unstructured":"H. Ehrig , K. Ehrig , C. Ermel , F. Hermann , and G. T\u00e4ntzer . 2007. Information preserving bidirectional model transformations. In FASE ."},{"key":"e_1_3_4_31_2","doi-asserted-by":"publisher","DOI":"10.5555\/1855347"},{"key":"e_1_3_4_32_2","volume-title":"Refactoring: Improving the Design of Existing Code","author":"Fowler M.","year":"2000","unstructured":"M. Fowler , K. Beck , J. Brant , W. Opdyke , and D. Roberts . 2000. Refactoring: Improving the Design of Existing Code . Addison-Wesley."},{"key":"e_1_3_4_33_2","volume-title":"UML Distilled: Applying the Standard Object Modeling Language","author":"Fowler M.","year":"1997","unstructured":"M. Fowler and S. Kendall . 1997. UML Distilled: Applying the Standard Object Modeling Language . Addison-Wesley Longman Ltd."},{"key":"e_1_3_4_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2003.1231152"},{"key":"e_1_3_4_35_2","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software","author":"Gamma E.","year":"1995","unstructured":"E. Gamma , R. Helm , R. Johnson , and J. Vlissides . 1995. Design Patterns: Elements of Reusable Object-Oriented Software . Addison-Wesley."},{"key":"e_1_3_4_36_2","volume-title":"ASE","author":"Gheyi R.","year":"2005","unstructured":"R. Gheyi , T. Massoni , and P. Borba . 2005. A rigorous approach for proving model refactorings. In ASE ."},{"key":"e_1_3_4_37_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.03.002"},{"key":"e_1_3_4_38_2","volume-title":"ASSE","author":"Golobisky M.","year":"2005","unstructured":"M. Golobisky and A. Vecchietti . 2005. Mapping UML class diagrams into object-relational schemas. In ASSE ."},{"key":"e_1_3_4_39_2","volume-title":"Program Restructuring as An Aid to Software Maintenance","author":"Griswold W.","year":"1991","unstructured":"W. Griswold . 1991. Program Restructuring as An Aid to Software Maintenance . Ph.D. Dissertation. University of Washington."},{"key":"e_1_3_4_40_2","volume-title":"BENEVOL","author":"Hassam K.","year":"2010","unstructured":"K. Hassam , S. Sadou , and R. Fleurquin . 2010. Adapting OCL constraints after a refactoring of their model using an MDE process. In BENEVOL ."},{"key":"e_1_3_4_41_2","article-title":"Formal analysis of model transformations based on triple graph grammars","volume":"24","author":"Hermann F.","year":"2012","unstructured":"F. Hermann , H. Ehrig , U. Golas , and F. Orejaso . 2012. Formal analysis of model transformations based on triple graph grammars. Mathematical Structures in Computer Science 24 (Jan. 2012).","journal-title":"Mathematical Structures in Computer Science"},{"key":"e_1_3_4_42_2","volume-title":"ECOOP","author":"Herrmannsd\u00f6rfer M.","year":"2009","unstructured":"M. Herrmannsd\u00f6rfer , S. Benz , and E. J\u00fcrgens . 2009. COPE\u2014automating coupled evolution of metamodels and models. In ECOOP ."},{"key":"e_1_3_4_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/505145.505149"},{"key":"e_1_3_4_44_2","doi-asserted-by":"publisher","DOI":"10.5555\/993772"},{"key":"e_1_3_4_45_2","doi-asserted-by":"publisher","DOI":"10.5555\/100511"},{"key":"e_1_3_4_46_2","volume-title":"ICSME","author":"Kim J.","year":"2015","unstructured":"J. Kim , D. Batory , and D. Dig . 2015. Scripting parametric refactorings in Java to retrofit design patterns. In ICSME ."},{"key":"e_1_3_4_47_2","volume-title":"ICSE","author":"Kim J.","year":"2016","unstructured":"J. Kim , D. Batory , D. Dig , and M. Azanza . 2016. Improving refactoring speed by 10X. In ICSE ."},{"key":"e_1_3_4_48_2","volume-title":"IWoR","author":"Kim J.","year":"2019","unstructured":"J. Kim , D. Batory , D. Dig , and M. Azanza . 2019. Code transformation issues in move-instance-method refactorings. In IWoR ."},{"key":"e_1_3_4_49_2","volume-title":"SBMF","author":"K\u00f6nig H.","year":"2011","unstructured":"H. K\u00f6nig , M. L\u00f6we , and C. Schulz . 2011. Model transformation and induced instance migration: A universal framework. In SBMF ."},{"key":"e_1_3_4_50_2","volume-title":"IWoR","author":"Lacker E.","year":"2021","unstructured":"E. Lacker , J. Kim , A. Kumar , L. Chandrashekar , S. Paramaiahgari , and J. Howard . 2021. Statistical analysis of refactoring bug reports in eclipse bugzilla. In IWoR ."},{"key":"e_1_3_4_51_2","article-title":"When and how to use multilevel modelling","author":"Lara J. De","year":"2014","unstructured":"J. De Lara , E. Guerra , and J. Cuadrado . 2014. When and how to use multilevel modelling. ACM ACM Transactions on Software Engineering and Methodology 24 (Dec.2014), 1\u201346.","journal-title":"ACM ACM Transactions on Software Engineering and Methodology"},{"key":"e_1_3_4_52_2","volume-title":"TASE","author":"Ledang H.","year":"2010","unstructured":"H. Ledang and H. Dubois . 2010. Proving model transformations. In TASE ."},{"key":"e_1_3_4_53_2","article-title":"Multi-view refactoring of class and activity diagrams using a multi-objective evolutionary algorithm","volume":"25","author":"Mansoor U.","year":"2015","unstructured":"U. Mansoor , M. Kessentini , M. Wimmer , and K. Deb . 2015. Multi-view refactoring of class and activity diagrams using a multi-objective evolutionary algorithm. Software Quality Journal 25 (Aug. 2015).","journal-title":"Software Quality Journal"},{"key":"e_1_3_4_54_2","volume-title":"AGTIVE","author":"Mantz F.","year":"2012","unstructured":"F. Mantz , S. Jurack , and G. T\u00e4ntzer . 2012. Graph transformation concepts for meta-model evolution guaranteeing permanent type conformance throughout model migration. In AGTIVE ."},{"key":"e_1_3_4_55_2","volume-title":"MODELS","author":"Maoz S.","year":"2011","unstructured":"S. Maoz , J. Ringert , and B. Rumpe . 2011. CD2Alloy: Class diagrams analysis using alloy revisited. In MODELS ."},{"key":"e_1_3_4_56_2","volume-title":"ECOOP","author":"Maoz S.","year":"2011","unstructured":"S. Maoz , J. Ringert , and B. Rumpe . 2011. CDDiff: Semantic differencing for class diagrams. In ECOOP ."},{"key":"e_1_3_4_57_2","article-title":"Refactoring OCL annotated UML class diagrams","author":"Markovi\u0107 S.","year":"2008","unstructured":"S. Markovi\u0107 and T. Baar . 2008. Refactoring OCL annotated UML class diagrams. Software and Systems Modeling 7 (Feb.2008), 25\u201347.","journal-title":"Software and Systems Modeling"},{"key":"e_1_3_4_58_2","doi-asserted-by":"publisher","DOI":"10.5555\/515230"},{"key":"e_1_3_4_59_2","volume-title":"SBES","author":"Massoni T.","year":"2005","unstructured":"T. Massoni , R. Gheyi , and P. Borba . 2005. Formal refactoring for UML class diagrams. In SBES ."},{"key":"e_1_3_4_60_2","volume-title":"Generic Model Management","author":"Melnik S.","year":"1998","unstructured":"S. Melnik . 1998. Generic Model Management , Lecture Notes in Computer Science, Vol. 2967. Springer-Verlag."},{"key":"e_1_3_4_61_2","doi-asserted-by":"publisher","DOI":"10.5555\/1007755"},{"key":"e_1_3_4_62_2","doi-asserted-by":"publisher","DOI":"10.1145\/1412331.1412334"},{"key":"e_1_3_4_63_2","article-title":"MS Access","year":"2020","unstructured":"Microsoft . 2020. MS Access. https:\/\/en.wikipedia.org\/wiki\/Microsoft_Access.","journal-title":"https:\/\/en.wikipedia.org\/wiki\/Microsoft_Access"},{"key":"e_1_3_4_64_2","article-title":"UML model refactoring: A systematic literature review","author":"Mohammed M.","year":"2015","unstructured":"M. Mohammed and A. Mohammad . 2015. UML model refactoring: A systematic literature review. Empirical Software Engineering (Jan.2015).","journal-title":"Empirical Software Engineering"},{"key":"e_1_3_4_65_2","volume-title":"HICSS","author":"Mok W.","year":"2001","unstructured":"W. Mok and D. Paper . 2001. On transformations from UML models to object-relational databases. In HICSS ."},{"key":"e_1_3_4_66_2","article-title":"The Vietnam of Computer Science","author":"Neward T.","year":"2006","unstructured":"T. Neward . 2006. The Vietnam of Computer Science. https:\/\/blogs.tedneward.com\/post\/the-vietnam-of-computer-science\/.","journal-title":"https:\/\/blogs.tedneward.com\/post\/the-vietnam-of-computer-science\/"},{"key":"e_1_3_4_67_2","unstructured":"Niols\n\t\t\t\t\t. 2016. \u2018\n\t\t\t\t\t\t\t \\(f\\_equal\\) \n\t\t\t\t\t\t\u2018 Isn\u2019t Doing Anything. (2016). Retrieved November 21 2019 from https:\/\/cstheory.stackexchange.com\/questions\/33743\/f-equal-isnt-doing-anything."},{"key":"e_1_3_4_68_2","article-title":"Meta-Object Facility (MOF) Specification, Version 2.0","author":"(OMG) O.","year":"2006","unstructured":"O. (OMG) . 2006. Meta-Object Facility (MOF) Specification, Version 2.0. OMG Document Number formal\/2006-01-01http:\/\/www.omg.org\/spec\/MOF\/2.0.","journal-title":"OMG Document Number formal\/2006-01-01"},{"key":"e_1_3_4_69_2","volume-title":"Refactoring Object-Oriented Frameworks","author":"Opdyke B.","year":"1992","unstructured":"B. Opdyke . 1992. Refactoring Object-Oriented Frameworks . Ph.D. Dissertation. University of Illinois at Urbana-Champaign."},{"key":"e_1_3_4_70_2","volume-title":"FASE","author":"Paige R.","year":"2001","unstructured":"R. Paige and J. Ostroff . 2001. Metamodelling and conformance checking with PVS. In FASE ."},{"key":"e_1_3_4_71_2","doi-asserted-by":"publisher","DOI":"10.5555\/119358"},{"key":"e_1_3_4_72_2","volume-title":"ASE","author":"Pilgrim J.","year":"2013","unstructured":"J. Pilgrim , B. Ulke , A. Thies , and F. Steimann . 2013. Model\/code co-refactoring: An MDE approach. In ASE ."},{"key":"e_1_3_4_73_2","volume-title":"EDBT","author":"Pottinger R.","year":"2008","unstructured":"R. Pottinger and P. Bernstein . 2008. Schema merging and mapping creation for relational sources. In EDBT ."},{"key":"e_1_3_4_74_2","volume-title":"Mylopoulos Festschrift, Conceptual Modeling: Foundations and Applications","author":"Pottinger R.","year":"2009","unstructured":"R. Pottinger and P. Bernstein . 2009. Associativity and commutativity in generic merge. In Mylopoulos Festschrift, Conceptual Modeling: Foundations and Applications , A. Borgida et\u00a0al. (Eds.), Lecture Notes in Computer Science, Vol. 5600. Springer-Verlag."},{"key":"e_1_3_4_75_2","volume-title":"ER","author":"Queralt A.","year":"2006","unstructured":"A. Queralt and E. Teniente . 2006. Reasoning on UML class diagrams with OCL constraints. In ER ."},{"key":"e_1_3_4_76_2","doi-asserted-by":"publisher","DOI":"10.5555\/929806"},{"key":"e_1_3_4_77_2","volume-title":"MODELS","author":"Rose L.","year":"2010","unstructured":"L. Rose et\u00a0al. 2010. A comparison of model migration tools. In MODELS ."},{"key":"e_1_3_4_78_2","volume-title":"ICMT","author":"Rose L. M.","year":"2010","unstructured":"L. M. Rose , D. S. Kolovos , R. F. Paige , and F. A. C. Polack . 2010. Model migration with epsilon flock. In ICMT ."},{"key":"e_1_3_4_79_2","volume-title":"Essential Scrum: A Practical Guide to the Most Popular Agile Process","author":"Rubin K.","year":"2012","unstructured":"K. Rubin . 2012. Essential Scrum: A Practical Guide to the Most Popular Agile Process . Addison-Wesley."},{"key":"e_1_3_4_80_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.03.006"},{"key":"e_1_3_4_81_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-12689-9_122"},{"key":"e_1_3_4_82_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2012.13"},{"key":"e_1_3_4_83_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2010.09.010"},{"key":"e_1_3_4_84_2","volume-title":"SFM","author":"Selic B.","year":"2012","unstructured":"B. Selic . 2012. The less well known UML. In SFM , M. Bernardo , V. Cortellessa , and A. Pierantonio (Eds.)."},{"key":"e_1_3_4_85_2","volume-title":"Database System Concepts","author":"Silberschatz A.","year":"2006","unstructured":"A. Silberschatz , H. Korth , and S. Sudarshan . 2006. Database System Concepts (5th ed.). McGraw-Hill, Inc."},{"key":"e_1_3_4_86_2","volume-title":"Software Engineering","author":"Sommerville I.","year":"1995","unstructured":"I. Sommerville . 1995. Software Engineering (5th ed.). Addison Wesley Longman Publishing Co., Inc., Chapter: Algebraic Specification."},{"key":"e_1_3_4_87_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59495-3"},{"key":"e_1_3_4_88_2","volume-title":"EMF: Eclipse Modeling Framework","author":"Steinberg D.","year":"2008","unstructured":"D. Steinberg and F. Budinsky . 2008. EMF: Eclipse Modeling Framework (2nd ed.). Addison-Wesley Professional."},{"key":"e_1_3_4_89_2","volume-title":"SoSYM","author":"Str\u00e4ten R.","year":"2007","unstructured":"R. Str\u00e4ten , V. Jonckers , and T. Mens . 2007. A formal approach to model refactoring and model refinement. In SoSYM ."},{"key":"e_1_3_4_90_2","volume-title":"PEPM","author":"Sultana N.","year":"2008","unstructured":"N. Sultana and S. Thompson . 2008. Mechanical verification of refactorings. In PEPM ."},{"key":"e_1_3_4_91_2","doi-asserted-by":"publisher","DOI":"10.5555\/1203067"},{"key":"e_1_3_4_92_2","volume-title":"ICGT","author":"T\u00e4ntzer G.","year":"2012","unstructured":"G. T\u00e4ntzer , F. Mantz , and Y. Lamo . 2012. Co-transformation of graphs and type graphs with application to model co-evolution. In ICGT ."},{"key":"e_1_3_4_93_2","volume-title":"ASE","author":"Tokuda L.","year":"1999","unstructured":"L. Tokuda and D. Batory . 1999. Evolving object-oriented designs with refactorings. In ASE ."},{"key":"e_1_3_4_94_2","volume-title":"ECOOP","author":"Wachsmuth G.","year":"2007","unstructured":"G. Wachsmuth . 2007. Metamodel adaptation and model co-adaptation. In ECOOP ."},{"key":"e_1_3_4_95_2","volume-title":"POPL","author":"Wang Y.","year":"2018","unstructured":"Y. Wang , I. Dillig , S. Lahiri , and W. Cook . 2018. Verifying equivalence of database-driven applications. In POPL ."},{"key":"e_1_3_4_96_2","unstructured":"Wikipedia\n\t\t\t\t\t. 2018. Partial Function. https:\/\/en.wikipedia.org\/wiki\/Partial_function."},{"key":"e_1_3_4_97_2","unstructured":"Wikipedia\n\t\t\t\t\t. 2019. Classical Logic. Retrieved December 12 2019 from https:\/\/en.wikipedia.org\/wiki\/Classical_logic."},{"key":"e_1_3_4_98_2","article-title":"Intuitionistic Logic","year":"2019","unstructured":"Wikipedia . 2019. Intuitionistic Logic. (2019). Retrieved September 11, 2019 from https:\/\/en.wikipedia.org\/wiki\/Intuitionistic_logic.","journal-title":"R"},{"key":"e_1_3_4_99_2","article-title":"Polymorphism","year":"2020","unstructured":"Wikipedia . 2020. Polymorphism. https:\/\/en.wikipedia.org\/wiki\/Polymorphism_(computer_science).","journal-title":"https:\/\/en.wikipedia.org\/wiki\/Polymorphism_(computer_science)"},{"key":"e_1_3_4_100_2","unstructured":"Wikipedia\n\t\t\t\t\t. 2021. Domain-Specific Language. https:\/\/en.wikipedia.org\/wiki\/Domain-specific_language."},{"key":"e_1_3_4_101_2","volume-title":"MODELSWARD","author":"Yu I.","year":"2015","unstructured":"I. Yu and H. Berg . 2015. A framework for metamodel composition and adaptation with conformance-preserving model migration. In MODELSWARD ."}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3549541","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3549541","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3549541","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:00:11Z","timestamp":1750186811000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3549541"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4,5]]},"references-count":100,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,4,30]]}},"alternative-id":["10.1145\/3549541"],"URL":"https:\/\/doi.org\/10.1145\/3549541","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,4,5]]},"assertion":[{"value":"2021-02-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-06-11","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-04-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}