A Theory of Least Change for Bidirectional Transformations

双向转换是维护多个信息源之间一致性的一种方法：当编辑一个信息源时，可能需要更新其他信息源以恢复一致性。有许多领域需要双向转换。目前，其中最著名的是模型驱动开发。模型驱动开发是一种开发软件的方法，其中模型——仅对要构建的软件的某些方面进行专门描述——是开发中的重要工件。部分或全部代码可以从模型中生成，而不是手工编写。不同的专家在不同的模型上工作，适应他们的需要，每个人都在自己的模型中记录他们的决定。为了最终得到一个正确的系统，模型需要保持一致；当一个开发人员更改一个模型时，可能需要更改另一个模型以匹配，反之亦然。另一个当前的应用是数据库中的“视图更新”问题（在编辑到视图表之后更新源表）。潜在的应用包括集成不同的电子健康记录，保持高级系统生物学模型与某些方面的更详细模型之间的一致性，提供对面向机器的数据表示的用户友好访问，自动化程序的协同进化及其正确性证明等。双向转换可以通过几个单向恢复功能来实现，每个源一个；但是这会复制信息（例如，在每个函数中都出现有关模型结构的信息），浪费精力并冒不一致的风险。双向转换语言允许使用单个声明性规范描述一致性关系和恢复函数。一个好的双向转换语言应该通过不允许开发人员编写无意义的内容来支持转换的开发人员：当根据该语言认为转换是正确的时，它应该遵守基本的完整性属性。双向变换的各种自然性质现在被很好地理解；特别是，“正确性”（双向转换确实恢复了一致性）和“希波克拉底性”（如果编辑的源代码保持一致，那么双向转换不会进行任何更改）。我们在这个项目中要研究的是“最小变化原则”（即双向转换在强制一致性时不应该进行不必要的更改）。我们的假设是：(i)最小变化原则可以被精确和有效地捕获；（ii）我们对原则的理解将受益于数据库中的“来源”工作——来源涉及建立和使用记录，记录哪些输出依赖于哪些输入，以及它们如何做到这一点；（iii）这将导致非自由数据类型（如关联列表和图）的“对齐”理论——部分的匹配。图是一种特别重要的数据类型，因为它们在软件工程中无处不在。特别地，模型驱动开发中的模型通常是图形类型，例如类图和状态图。这个项目将研究双向变换的数学基础。这样做的原因是为了更好地理解最小变更原则，在将来，有助于更可用和更可靠的模型驱动的工程工具，支持有效和正确的软件开发，即使面对持续的变更。因此，它将使软件开发人员能够将模型驱动开发的优点与敏捷方法的优点结合起来。通过开发更好的语言和工具，它还将使双向转换在广泛的其他应用领域的使用变得切实可行。

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.