2014 | OriginalPaper | Buchkapitel
Validity Checking of Putback Transformations in Bidirectional Programming
verfasst von : Zhenjiang Hu, Hugo Pacheco, Sebastian Fischer
Erschienen in: FM 2014: Formal Methods
Verlag: Springer International Publishing
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.