A verified catalogue of OCL optimisations

  • PDF / 1,526,740 Bytes
  • 23 Pages / 595.276 x 790.866 pts Page_size
  • 10 Downloads / 192 Views

DOWNLOAD

REPORT


SPECIAL SECTION PAPER

A verified catalogue of OCL optimisations Jesús Sánchez Cuadrado1 Received: 7 February 2019 / Revised: 13 June 2019 / Accepted: 20 June 2019 © Springer-Verlag GmbH Germany, part of Springer Nature 2019

Abstract OCL is widely used by model-driven engineering tools with different purposes like writing integrity constraints for metamodels, as a navigation language in model transformation languages or to define transformation specifications. Another scenario is the automatic generation of OCL code by a repair system. These generated expressions tend to be complex and unreadable due to the nature of the generative process. However, to be useful this code should be simple and resemble manually written code as much as possible when a developer must manually maintain it. There exists refactorings approaches for manually written OCL code, but there is no tool targeted to the optimisation of OCL expressions which have been automatically synthesised. Moreover, there is no available catalogue of OCL refactorings which can be integrated seamlessly into a tool. In this work, we contribute a set of refactorings intended to optimise OCL expressions, notably covering cases likely to arise in generated OCL code. We also contribute the implementation of these refactorings, built as a generic transformation catalogue using bento¯ , a transformation reuse tool for ATL. This makes it possible to specialise the catalogue for any OCL variant based on Ecore. Moreover, we propose a method to verify the correctness of the implemented catalogue based on translation validation and model finding. We describe the design and implementation of the catalogue and evaluate it by optimising a large amount of OCL expressions and proving the correctness of each optimisation execution. We also derive working implementations of the catalogue for ATL, EMF/OCL and SimpleOCL made available in a tool called BeautyOCL. Keywords Model transformations · OCL · Refactoring · Verification

1 Introduction OCL [39] is used in model-driven engineering (MDE) in a wide range of scenarios, such as the definition of integrity constraints for meta-models and UML models, to navigate models in model transformation languages and as input for model finders, among others. The most usual scenario is that OCL constraints are written by developers who can choose their preferred style, and thus tend to write concise and readable code. A completely different scenario is the automatic generation of OCL constraints. In this setting, the style of Communicated by Prof. A. Pierantonio, A. Anjorin, S. Trujillo, and H. Espinoza. Work funded by project RECOM (Spanish MINECO, TIN2015-73968-JIN, AEI/FEDER/UE) and a Ramón y Cajal 2017 grant (RYC-2017-237) co-funded by MINECO (Spain) and the European Social Fund.

B 1

Jesús Sánchez Cuadrado [email protected]

the generated constraints is frequently sub-optimal, in the sense that it may contain repetitive expressions, unnecessary constructs (e.g. too many let expressions), trivial expressions (e.g. false = false), etc. This i