T1 - Formalizing and Reasoning about Bidirectional Transformations

Likewise to the functional subset, this research team has considerable expertise in using the PF relational calculus to reason about disparate application domains [3]. Building on this expertise, the first objective of this task is to show its potential for formalizing and reasoning about bidirectional transformations. To be more specific, we intend to:

• Show how this calculus can be used to derive correct-by-construction bidirectional implementations from relational specifications. The typical approach to design a bidirectional language is to define a set of primitive transformations and combinators, and then prove by hand that the former satisfy the desired properties and that the latter preserve them. For some more complex scenarios (for example, the lenses for defining views on relational databases [10]) such proofs are far from trivial and are usually omitted, Moreover, it is not clear why a particular functional implementation is picked given the apparent non-determinism of the original specification. Using the PF relational calculus we intend to recast such works, shedding new light on some of the decisions, and avoiding the a posteriori proofs by deriving correct implementations from specifications.
• Simplify the formalization of some issues that are transversal to the field, namely alignment and data redundancy. Establishing the connection between similar elements in the source and target models (alignment) is fundamental for defining accurate backward transformations. This issue is usually left implicit in most bidirectional languages, but some works are emerging where alignment is explicitly formalized [11,13]. As shown in [13] alignment can be intuitively expressed using sameness relations. Concerning redundancy, quotient lenses [12] already showed how equivalence relations can be used to relax bidirectional laws in order to be insensitive to irrelevant model details. We believe the PF style can make the formalization of these issues simpler and speed up proofs.
• Show the formal connection between different axiomatizations of bidirectionality. There is no consensus in the community about the formal requirements of a bidirectional transformation framework. Each new system tends to introduce slight variations in the axiomatization of such requirements, making it very difficult for end-users to decide which systems best match their needs. Diskin [9] has already proposed an algebraic framework in which some bidirectional axiomatizations can be compared and analyzed. Using the PF style we intend to simplify and extend his work.

Equipped with this unifying formalism, the second objective of this task is to write a comprehensive survey of the area. Although relatively recent, the body of work is growing exponentially, making it increasingly difficult for end-users and new researchers to dip into the area. The few existing surveys [8] are mere enumerations of existing work, lacking proper taxonomies and metrics to classify and compare the different approaches. To maximize the relevance and impact of the survey, the renowned international consultants of the project will be actively involved in its preparation.

The expected deliverables of this task are:

• Two international conference papers showing how the PF relational calculus can be used to formalize and reason about bidirectional transformations.
• An international journal paper with a comprehensive survey of the area.

José Nuno Oliveira will be responsible for this task due to his renowned expertise on the PF relational calculus. The the bulk of the work concerning the first objective will be performed by Nuno Macedo, who has just started a PhD precisely on using the PF relational calculus to formalize and reason about bidirectional transformations. Hugo Pacheco and Jácome Cunha will be involved in writing up the survey, given their recent PhDs on related subjects. Alcino Cunha will also be involved due to his longterm research on bidirectional transformations.

Team

• José Nuno Oliveira
• Manuel Alcino Cunha
• Hugo Pacheco
• Jácome Cunha
• Nuno Macedo [PhD]