Summer School on Bidirectional Transformations

Bx with Triple Graph Grammars

Triple Graph Grammars (TGGs) provide a rule-based means of specifying a consistency relation over two graph languages. TGG rules are direction agnostic, describing the simultaneous creation of pairs of consistent graphs in both languages. Correspondences between elements in the different languages are thereby represented explicitly as a third “correspondence” graph.

Many useful tools can be derived automatically from a TGG including an instance generator, consistent forward and backward transformations, and incrementally working synchronisers, which are able to realise forward and backward change propagation without incurring unnecessary information loss.

In this lecture, TGGs will be introduced as a pragmatic implementation of the symmetric delta lens framework (proposed by Diskin et al.). To complement this theoretical foundation, a hands-on session and carefully chosen examples will be used to develop a practical intuition for TGGs, using eMoflon — one of many actively developed TGG tools.

Materials: Virtual machine; Lecture 1; Lecture 2; Lecture 3

Modular Edit Lenses

These talks will present the edit lens framework by Wagner, Pierce, MH [HPW], and compare it to other approaches. After briefly recapitulating symmetric lense and their relationship to asymmetric lenses and constraint maintainers we define the HPW edit lenses based on monoids of edit operations. We explain the relationship to other approaches to edit operations notably those based on categories and on exact sequences. We then focus on the modular nature of HPW edit lenses by presenting various lens combinators for container-like data structures. In the last lecture we will present loose ends and open problems.

Materials: Slides

Principles and Practice of Putback-based Bidirectional Programming in BiGUL

Putback-based bidirectional programming allows the programmer to write only one putback transformation, from which the unique corresponding forward transformation is derived for free. A key distinguishing feature of putback-based bidirectional programming is its full control over the bidirectional behavior, which is important to specify intended bidirectional transformations without any ambiguity.

In this tutorial, we will introduce BiGUL, a simple but powerful putback-based bidirectional programming language, explaining its principle, showing how to develop various of bidirectional transformations in BiGUL, demonstrating its application to adaptive software development, and highlighting important issues and challenges for future work.

This tutorial will be given jointly with Hsiang-Shang Ko.

Materials: Putback-Based BX website; source materials; slides for Lecture 1, Lecture 2, and Lecture 3

Mathematical Foundations of Bidirectional Transformations

This series of lectures presents a range of mathematical analyses of bidirectional transformations. The aim is to be self-contained (so that no significant mathematical prerequisites are expected), and to present sufficient material to reach some of the open questions in the field. The mathematical analysis of bidirectional transformations is intended to revise, simplify and systematise participants' knowledge of bidirectional transformations gained in other lectures. The focus is on techniques that have wide application.

Materials: Lecture 1; Lecture 2; Lecture 3; Exercises

Engineering Bidirectional Transformations

Bidirectional transformations are artifacts that can (and probably should) be engineered, following a suitable lifecycle. In these lectures, we consider different phases of a BX engineering lifecycle, and explore ways in which the requirements, architectures, designs and implementations of BX can be specified, and support that can be used to help verify or validate such artifacts.

Materials: Lecture 1; Lecture 2; Lecture 3

Introduction, TLCBX Results, Conclusion

The TLCBX team will have three lecture slots at the school. The first slot of the week will introduce general notions of BX (including the view-update problem, the relational perspective via consistency restoration, varieties of lens, and triple graph grammars), in order to establish a common foundation and highlight some differences in approach for the week; in particular, we will summarize our own work on effectful lenses and the entangled state monad. A second slot will cover recent work focussing on complement structures as witnesses to consistency, including the use of dependent types (with witnesses more specifically to proofs of consistency). In the final slot of the week, we will discuss our work on the least change principle in BX and on BX's potential to transform the development and use of software, drawing out and bringing together some common threads in the other lecturers' sessions.

Materials: Welcome; Introduction; Entangled State; Dependent Types; Least Change