A Theory of Least Change for Bidirectional Transformations

A bidirectional transformation is a means of maintaining consistency between multiple information sources: when one source is edited, the others may need updating to restore consistency. There are many domains in which bidirectional transformations are needed. Currently, the best-known of these is model-driven development. Model-driven development is the approach to developing software in which models - specialised descriptions of only certain aspects of the software to be built - are important artefacts in the development. Some or all code may be generated from models, rather than written by hand. Different experts work on different models, adapted to their needs, each recording their decisions in their own model. In order to end up with a correct system, the models need to be kept consistent; when one developer changes one model, another model may need to be changed to match, and vice versa. Another current application is the "view update" problem in databases (updating source tables after edits to view tables). Potential applications include integrating different electronic health records, maintaining consistency between a high-level systems biology model and a more detailed model of some aspect, providing user-friendly access to machine-oriented data representation, automating the coevolution of a program with its proof of correctness, etc.

A bidirectional transformation can be implemented in terms of several unidirectional restoring functions, one per source; but this duplicates information (for example, information about the structure of the models being related appears in every function), wasting effort and risking inconsistencies. Bidirectional transformation languages allow one to describe the consistency relationship and the restoring functions with a single declarative specification. A good bidirectional transformation language should support the developer of the transformation by not allowing the developer to write nonsense: when a transformation is considered correct according to the language, it should obey basic sanity properties.

Various natural properties of bidirectional transformations are now well understood; in particular, "correctness" (that the bidirectional transformation does actually restore consistency) and "hippocraticness" (that if an edited source remains consistent, then the bidirectional transformation makes no changes). What is much less well understood, and what we will study in this project, is the "principle of least change" (that a bidirectional transformation should not make unnecessary changes when it enforces consistency).

Our hypotheses are: (i) that this Principle of Least Change can be precisely and productively captured; (ii) that our understanding of the Principle will benefit from work on "provenance" in databases - provenance involves building and using a record of which outputs depend on which inputs, and how they do so; and (iii) that this will lead to a theory of "alignment" - matching of parts - for non-free datatypes such as associative lists and graphs. Graphs are an especially important datatype, because they are ubiquitous in software engineering. In particular, the models in model-driven development are often types of graph, such as class diagrams and statecharts.This project will work on the mathematical foundations of bidirectional transformations. The reason for doing this is in order that a better understanding of the Principle of Least Change will, in future, contribute to more usable and more reliable model-driven engineering tools, supporting efficient and correct software development, even in the face of continuous change. It will thus enable software developers to combine the advantages of model-driven development with those of agile methods. By enabling better languages and tools to be developed, it will also make practical the use of bidirectional transformations in a wide range of other application areas.