A Theory of Least Change for Bidirectional Transformations
Lead Research Organisation:
University of Oxford
Department Name: Computer Science
Abstract
Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.
Organisations
Publications
Abou-Saleh F
(2018)
Bidirectional Transformations
Abou-Saleh F
(2017)
Coalgebraic Aspects of Bidirectional Computation.
in The Journal of Object Technology
Abou-Saleh F
(2016)
A List of Successes That Can Change the World
Abou-Saleh Faris
(2016)
Reflections on Monadic Lenses
in arXiv e-prints
Abou-Saleh, F
(2015)
Coalgebraic Aspects of Bidirectional Computation
Boisseau G
(2018)
What you needa know about Yoneda: profunctor optics and the Yoneda lemma (functional pearl)
in Proceedings of the ACM on Programming Languages
Cheney J
(2014)
Entangled State Monads
Cheney J
(2014)
Towards a Repository of BX Examples
Cheney J
(2017)
On principles of Least Change and Least Surprise for bidirectional transformations.
in The Journal of Object Technology
| Description | We have discovered that the technical device called monads can be useful to describe, formally, correctness properties for the type of software artefact we're studying (bidirectional transformations). These are particularly useful in that, we showed, they can be used to reason about situations in which the bidirectional transformation needs to have so-called effects, such as interacting with the user. We have developed several notions of least surprise; that is, properties that can help such bidirectional transformations to have behaviour that will be useful and not disruptive to their users. We showed why the most obvious version of such a property does not always give the bidirectional transformation the best behaviour, and we investigated alternatives deriving from mathematical analysis. We have developed the concept of subspace pairs, which help us to describe situations in which a bidirectional transformation may have very safe, predictable behaviour under some circumstances, so that the user could feel confident in using it without checking under those circumstances, while under other circumstances it may be necessary for the user to check whether the transformation's behaviour is what is wanted. Unexpectedly, we found a close relationship between bidirectional transformations and a well-known relationship between concurrent processes, viz bisimulation. In a nutshell, bidirectional transformations are proof-relevant bisimulations; here proof-relevant means that it does not only matter that things are related, but precisely how they are related. We found several areas that need more investigation than we could do on this grant: for example, we found that witness structures, which help to demonstrate whether data sources are consistent, can be described using dependent types; we now hypothesise that it will be important for a bidirectional transformation to explain its actions, and we think an approach via dependent types may help us to do this. |
| Exploitation Route | Our findings will help people who design bidirectional transformation languages (including, we hope, ourselves) to make choices that will make the languages easy to use to write bidirectional transformations that will do what users want without confusing or surprising them. Such languages may be embedded in a general purpose programming language such as Haskell, making use of our monad-based work, or may be free-standing languages. This is one ingredient in an ongoing agenda of helping model-driven development to be more generally applicable in an agile way, thereby making it feasible to develop high quality software faster and more cheaply. |
| Sectors | Digital/Communication/Information Technologies (including Software) |
| Description | Please see the impact description provided for EP/K020218/1. |
| First Year Of Impact | 2016 |
| Sector | Digital/Communication/Information Technologies (including Software) |
| Title | BX Repository |
| Description | This is primarily a theoretical, foundational project. However, we have established the Bx Example Repository, which is a resource for the whole community interested in bidirectional transformations, including both theoreticians and practitioners. It records and discusses interesting examples of bidirectional transformations, some theoretical, some industrial in origin. |
| Type Of Technology | Software |
| Year Produced | 2014 |
| Open Source License? | Yes |
| Impact | N/A |
| URL | http://bx-community.wikidot.com/examples:home |