Summary

With the ever growing list of programming languages and software development frameworks, transforming a data model into a different format is essential to "bridge the gap" between technology layers and enable information sharing among applications. Ideally, these transformations should be bidirectional, allowing changes to a model to be safely propagated to another. The naive approach to bidirectional transformation (BT) is to engineer two unidirectional transformations together and manually prove that they are consistent according to the required round-tripping axioms. This gives rise to maintenance problems, besides being notoriously expensive and error-prone: any change in a data format implies a redefinition of both transformations, and a new consistency proof. A better approach is to design a domain-specific language in which one expression denotes both transformations, ensured consistent by construction.

The BT research community is growing by the day, with new languages and frameworks being proposed to tackle the most diverse scenarios. This project aims to extend such coverage and propose effective BT frameworks for three relevant application domains: model-driven engineering (MDE), spreadsheet validation and transformation, and language-based editors (LBEs) defined with attribute grammars (AGs).

MDE prescribes the use of automatic model transformations to generate correct implementations by step-wise refinement of high-level platform independent models. Managing model inconsistency is a key issue and several ad-hoc techniques for model/code synchronization and round-trip engineering have been proposed. BT address this problem upfront, and increasing effort is being dedicated by the MDE community to the design of bidirectional model transformation languages. Unfortunately, these are still plagued with semantic ambiguities or expressiveness limitations that outlaw many interesting problems. A main aim of this project is thus to define a model transformation language with precise bidirectional semantics, expressive enough to handle classic MDE scenarios.

Spreadsheets are widely used by non-professional programmers to develop business applications. These programmers vastly outnumber the professional ones and create millions of spreadsheets every year. Spreadsheets are quite flexible, but they are also very error prone. Spreadsheet models specifying the business logic can prevent errors and improve users productivity. Unfortunately, manually synchronizing such models and instances is a complex task. Moreover, the spreadsheet model may evolve over time and, therefore, the data has to be adapted to conform to the new model. In this project we intend to apply BTs not only to automate such synchronization and evolution, but also to allow collaborative editing of different views of the same spreadsheet.

The definition of LBEs is a well-known application of AGs. The AG and the derived editor define a unidirectional transformation: users can edit the source program and the target one is automatically (and incrementally) synchronized after user interaction; however, they are still unable to synchronize the source program after a change in the target. This problem could be addressed by developing a BT system for AGs. Surprisingly, despite the existence of prototype bidirectional LBEs, little work has been done in defining generic BT mechanisms specifically for AGs. That is the research direction we intend to follow in this project, and we expect such a mechanism to be a major contribution to the overall AG community.

Common to these application domains is the fact that models cannot be captured by pure hierarchical (tree-like) data structures. Of course, they can be represented in XML-like formats by relying on internal key references to model circularity or sharing between elements. Although effective BT frameworks have been proposed to handle hierarchical models, no generic and effective framework has yet been proposed for non-hierarchical ones. We intend to do so by relying on the point-free (PF) relational calculus, a quantifier free formalization of first-order logic, popularized in the algebra of programming community. This calculus deals naturally with non-determinism and partiality, two key issues in the formalization of BTs. It is also amenable to calculation thanks to its purely equational reasoning style, which opens interesting opportunities for BT optimization.