Validity Checking of Putback Transformations in Bidirectional Programming

A bidirectional transformation consists of pairs of transformations —a forward transformation

get

produces a target view from a source, while a putback transformation

put

puts back modifications on the view to the source— satisfying sensible roundtrip properties. Existing bidirectional approaches are

get

-based in that one writes (an artifact resembling) a forward transformation and a corresponding backward transformation can be automatically derived. However, the unavoidable ambiguity that stems from the underspecification of

put

often leads to unpredictable bidirectional behavior, making it hard to solve nontrivial practical synchronization problems with existing bidirectional transformation approaches. Theoretically, this ambiguity problem could be solved by writing

put

directly and deriving

get

, but differently from programming with

get

it is easy to write invalid

put

functions. An open challenge is how to check whether the definition of a putback transformation is valid, while guaranteeing that the corresponding unique

get

exists. In this paper, we propose, as far as we are aware, the first

safe

language for supporting putback-based bidirectional programming. The key to our approach is a simple but powerful language for describing primitive putback transformations. We show that validity of putback transformations in this language is decidable and can be automatically checked. A particularly elegant and strong aspect of our design is that we can simply reuse and apply standard results for treeless functions and tree transducers in the specification of our checking algorithms.