Abstract
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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bancilhon, F., Spyratos, N.: Update semantics of relational views. ACM Transactions on Database Systems 6(4), 557–575 (1981)
Barbosa, D.M.J., Cretin, J., Foster, J.N., Greenberg, M., Pierce, B.C.: Matching lenses: alignment and view update. In: ICFP 2010, pp. 193–204. ACM (2010)
Bohannon, A., Foster, J.N., Pierce, B.C., Pilkiewicz, A., Schmitt, A.: Boomerang: resourceful lenses for string data. In: POPL 2008, pp. 407–419. ACM (2008)
Bohannon, A., Pierce, B.C., Vaughan, J.A.: Relational lenses: a language for updatable views. In: PODS 2006, pp. 338–347. ACM (2006)
Buneman, P., Cheney, J., Vansummeren, S.: On the expressiveness of implicit provenance in query and update languages. ACM Transactions on Database Systems 33(4) (2008)
Czarnecki, K., Foster, J.N., Hu, Z., Lämmel, R., Schürr, A., Terwilliger, J.: Bidirectional transformations: A cross-discipline perspective. In: Paige, R.F. (ed.) ICMT 2009. LNCS, vol. 5563, pp. 260–283. Springer, Heidelberg (2009)
Dayal, U., Bernstein, P.: On the correct translation of update operations on relational views. ACM Transactions on Database Systems 7, 381–416 (1982)
Fischer, S., Hu, Z., Pacheco, H.: “Putback” is the Essence of Bidirectional Programming. GRACE Technical Report 2012-08, National Institute of Informatics, 36 p. (2012)
Foster, J.: Bidirectional Programming Languages. Ph.D. thesis, University of Pennsylvania (December 2009)
Foster, J.N., Greenwald, M.B., Moore, J.T., Pierce, B.C., Schmitt, A.: Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem. ACM Transactions on Programming Languages and Systems 29(3), 17 (2007)
Giesl, J., Kapur, D.: Decidable classes of inductive theorems. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 469–484. Springer, Heidelberg (2001)
Gottlob, G., Paolini, P., Zicari, R.: Properties and update semantics of consistent views. ACM Transactions on Database Systems 13(4), 486–524 (1988)
Hidaka, S., Hu, Z., Inaba, K., Kato, H., Matsuda, K., Nakano, K.: Bidirectionalizing graph transformations. In: ICFP 2010, pp. 205–216. ACM (2010)
Hofmann, M., Pierce, B.C., Wagner, D.: Symmetric lenses. In: POPL 2011, pp. 371–384. ACM (2011)
Hofmann, M., Pierce, B.C., Wagner, D.: Edit lenses. In: POPL 2012, pp. 495–508. ACM (2012)
Hu, Z., Schürr, A., Stevens, P., Terwilliger, J.F.: Dagstuhl Seminar on Bidirectional Transformations (BX). SIGMOD Record 40(1), 35–39 (2011)
Hu, Z., Mu, S.C., Takeichi, M.: A programmable editor for developing structured documents based on bidirectional transformations. Higher-Order and Symbolic Computation 21(1-2), 89–118 (2008)
Hutton, G.: Programming in Haskell. Cambridge University Press (2007)
Kühnemann, A.: Comparison of deforestation techniques for functional programs and for tree transducers. In: Middeldorp, A., Sato, T. (eds.) FLOPS 1999. LNCS, vol. 1722, pp. 114–130. Springer, Heidelberg (1999)
Lämmel, R.: Coupled Software Transformations (Extended Abstract). In: SETS 2004 (2004)
Matsuda, K., Hu, Z., Nakano, K., Hamana, M., Takeichi, M.: Bidirectionalization transformation based on automatic derivation of view complement functions. In: ICFP 2007, pp. 47–58. ACM (2007)
Meertens, L.: Designing constraint maintainers for user interaction (1998), manuscript available at, http://www.kestrel.edu/home/people/meertens
Pacheco, H., Cunha, A.: Generic point-free lenses. In: Bolduc, C., Desharnais, J., Ktari, B. (eds.) MPC 2010. LNCS, vol. 6120, pp. 331–352. Springer, Heidelberg (2010)
Pacheco, H., Cunha, A., Hu, Z.: Delta lenses over inductive types. In: BX 2012. Electronic Communications of the EASST, vol. 49 (2012)
Pacheco, H., Hu, Z., Fischer, S.: Monadic combinators for “putback” style bidirectional programming. In: PEPM 2014, pp. 39–50. ACM (2014)
Seidl, H.: Single-valuedness of tree transducers is decidable in polynomial time. Theor. Comput. Sci. 106(1), 135–181 (1992)
Voigtländer, J.: Bidirectionalization for free! (pearl). In: POPL 2009, pp. 165–176. ACM (2009)
Wadler, P.: Deforestation: Transforming programs to eliminate trees. In: Ganzinger, H. (ed.) ESOP 1988. LNCS, vol. 300, pp. 344–358. Springer, Heidelberg (1988)
Xiong, Y., Liu, D., Hu, Z., Zhao, H., Takeichi, M., Mei, H.: Towards automatic model synchronization from model transformations. In: ASE 2007, pp. 164–173. ACM (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Hu, Z., Pacheco, H., Fischer, S. (2014). Validity Checking of Putback Transformations in Bidirectional Programming. In: Jones, C., Pihlajasaari, P., Sun, J. (eds) FM 2014: Formal Methods. FM 2014. Lecture Notes in Computer Science, vol 8442. Springer, Cham. https://doi.org/10.1007/978-3-319-06410-9_1
Download citation
DOI: https://doi.org/10.1007/978-3-319-06410-9_1
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-06409-3
Online ISBN: 978-3-319-06410-9
eBook Packages: Computer ScienceComputer Science (R0)