An axiomatic basis for bidirectional programming

Abstract

Among the frameworks of bidirectional transformations proposed for addressing various synchronisation (consistency maintenance) problems, Foster et al.’s [2007] asymmetric lenses have influenced the design of a generation of bidirectional programming languages. Most of these languages are based on a declarative programming model, and only allow the programmer to describe a consistency specification with ad hoc and/or awkward control over the consistency restoration behaviour. However, synchronisation problems are diverse and require vastly different consistency restoration strategies, and to cope with the diversity, the programmer must have the ability to fully control and reason about the consistency restoration behaviour. The putback-based approach to bidirectional programming aims to provide exactly this ability, and this paper strengthens the putback-based position by proposing the first fully fledged reasoning framework for a bidirectional language — a Hoare-style logic for Ko et al.’s [2016] putback-based language BiGUL. The Hoare-style logic lets the BiGUL programmer precisely characterise the bidirectional behaviour of their programs by reasoning solely in the putback direction, thereby offering a unidirectional programming abstraction that is reasonably straightforward to work with and yet provides full control not achieved by previous approaches. The theory has been formalised and checked in Agda, but this paper presents the Hoare-style logic in a semi-formal way to make it easily understood and usable by the working BiGUL programmer.

References

1. Davi M. J. Barbosa, Julien Cretin, Nate Foster, Michael Greenberg, and Benjamin C. Pierce. 2010. Matching Lenses: Alignment and View Update. In International Conference on Functional Programming (ICFP’10). ACM, 193–204.
2. Aaron Bohannon, J. Nathan Foster, Benjamin C. Pierce, Alexandre Pilkiewicz, and Alan Schmitt. 2008. Boomerang: Resourceful Lenses for String Data. In Symposium on Principles of Programming Languages (POPL’08). ACM, 407–419.
3. Aaron Bohannon, Benjamin C. Pierce, and Jeffrey A. Vaughan. 2005. Relational Lenses: A Language for Updatable Views. Technical Report. Department of Computer and Information Science, University of Pennsylvania. http://www.cis.upenn. edu/~bcpierce/papers/dblenses-tr.pdf
4. Aaron Bohannon, Benjamin C. Pierce, and Jeffrey A. Vaughan. 2006. Relational Lenses: A Language for Updatable Views. In Symposium on Principles of Database Systems (PODS’06) . ACM, 338–347.
5. Venanzio Capretta. 2005. General Recursion via Coinductive Types. Logical Methods in Computer Science 1, 2 (2005), 1–28.
6. James Cheney, Jeremy Gibbons, James McKinna, and Perdita Stevens. 2017. On Principles of Least Change and Least Surprise for Bidirectional Transformations. Journal of Object Technology 16, 1 (2017), 3:1–31.
7. Kevin Colson, Robin Dupuis, Lionel Montrieux, Zhenjiang Hu, Sebastián Uchitel, and Pierre-Yves Schobbens. 2016. Reusable Self-Adaptation through Bidirectional Programming. In International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS’16) . ACM, 4–15.
8. Krzysztof Czarnecki, J. Nathan Foster, Zhenjiang Hu, Ralf Lämmel, Andy Schürr, and James F. Terwilliger. 2009. Bidirectional Transformations: A Cross-Discipline Perspective. In International Conference on Model Transformation (Lecture Notes in Computer Science) , Vol. 5563. Springer, 260–283.
9. Edsger W. Dijkstra. 1974. Programming as a Discipline of Mathematical Nature. Amer. Math. Monthly 81, 6 (1974), 608–612.
10. Zinovy Diskin, Yingfei Xiong, and Krzysztof Czarnecki. 2011. From State- to Delta-Based Bidirectional Model Transformations: the Asymmetric Case. Journal of Object Technology 10 (2011), 6:1–25.
11. Sebastian Fischer, Zhenjiang Hu, and Hugo Pacheco. 2015a. A Clear Picture of Lens Laws. In International Conference on Mathematics of Program Construction (Lecture Notes in Computer Science) , Vol. 9129. Springer, 215–223.
12. Sebastian Fischer, Zhenjiang Hu, and Hugo Pacheco. 2015b. The Essence of Bidirectional Programming. SCIENCE CHINA Information Sciences 58, 5 (2015), 1–21.
13. John Nathan Foster. 2009. Bidirectional Programming Languages. Ph.D. Dissertation. University of Pennsylvania. http: //repository.upenn.edu/edissertations/56
14. J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce, and Alan Schmitt. 2007. Combinators for Bidirectional Tree Transformations: A Linguistic Approach to the View-Update Problem. ACM Transactions on Programming Languages and Systems 29, 3 (2007), 17.
15. Nate Foster, Kazutaka Matsuda, and Janis Voigtländer. 2012. Three Complementary Approaches to Bidirectional Programming. In Generic and Indexed Programming. Lecture Notes in Computer Science, Vol. 7470. Springer, 1–46.
16. Jeremy Gibbons. 2007. Datatype-Generic Programming. In Datatype-Generic Programming. Lecture Notes in Computer Science, Vol. 4719. Springer, 1–71.
17. C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming. Commun. ACM 12, 10 (1969), 576–580.
18. Martin Hofmann, Benjamin Pierce, and Daniel Wagner. 2011. Symmetric Lenses. In Symposium on Principles of Programming Languages (POPL’11) . ACM, 371–384.
19. Zhenjiang Hu and Hsiang-Shang Ko. 2017. Principles and Practice of Bidirectional Programming in BiGUL. Draft lecture notes for the Oxford Summer School on Bidirectional Transformations. https://bitbucket.org/prl_tokyo/bigul/raw/master/ SSBX16/tutorial.pdf
20. Zhenjiang Hu, Hugo Pacheco, and Sebastian Fischer. 2014. Validity Checking of Putback Transformations in Bidirectional Programming. In International Symposium on Formal Methods (Lecture Notes in Computer Science), Vol. 8442. Springer, 1–15.
21. Daisuke Kinoshita and Keisuke Nakano. 2017. Bidirectional Certified Programming. In International Workshop on Bidirectional Transformations (BX’17) . CEUR-WS.org, 31–38. http://ceur-ws.org/Vol-1827/paper7.pdf
22. Hsiang-Shang Ko, Tao Zan, and Zhenjiang Hu. 2016. BiGUL: A Formally Verified Core Language for Putback-Based Bidirectional Programming. In Workshop on Partial Evaluation and Program Manipulation (PEPM’16). ACM, 61–72.
23. Nuno Macedo, Hugo Pacheco, Alcino Cunha, and José N. Oliveira. 2013. Composing Least-Change Lenses. In International Workshop on Bidirectional Transformations (Electronic Communications of the EASST) . EASST.
24. Kazutaka Matsuda and Meng Wang. 2015. Applicative Bidirectional Programming with Lenses. In International Conference on Functional Programming (ICFP’15) . ACM, 62–74.
25. James McKinna. 2016. Bidirectional Transformations are Proof-Relevant Bisimulations (Extended Abstract). In International Workshop on Type-Driven Development (TyDe’16) . http://groups.inf.ed.ac.uk/bx/TyDe16.pdf
26. Jorge Mendes, Hsiang-Shang Ko, and Zhenjiang Hu. 2016. The Under-Appreciated Put: Implementing Delta-Alignment in BiGUL . Technical Report GRACE-TR 2016-03. GRACE Center, National Institute of Informatics. http://grace-center.jp/ wp-content/uploads/2016/04/GRACE-TR-2016-03.pdf
27. Hugo Pacheco, Alcino Cunha, and Zhenjiang Hu. 2012. Delta Lenses over Inductive Types. In International Workshop on Bidirectional Transformations . EASST.
28. Hugo Pacheco, Zhenjiang Hu, and Sebastian Fischer. 2014a. Monadic Combinators for “Putback” Style Bidirectional Programming. In Workshop on Partial Evaluation and Program Manipulation (PEPM’14). ACM, 39–50.
29. Hugo Pacheco, Tao Zan, and Zhenjiang Hu. 2014b. BiFluX: A Bidirectional Functional Update Language for XML. In International Symposium on Principles and Practice of Declarative Programming (PPDP’14) . ACM, 147–158.
30. John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In Symposium on Logic in Computer Science (LICS’02) . IEEE, 55–74.
31. Perdita Stevens. 2010. Bidirectional Model Transformations in QVT: Semantic Issues and Open Questions. Software and Systems Modeling 9 (2010), 7.
32. Michael Kirkedal Thomsen and Holger Bock Axelsen. 2015. Interpretation and Programming of the Reversible Functional Language RFUN. In Symposium on the Implementation and Application of Functional Programming Languages (IFL’15). ACM.
33. Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton Jones. 2014. Refinement Types for Haskell. In International Conference on Functional Programming (ICFP’14) . ACM, 269–282.
34. Janis Voigtländer, Zhenjiang Hu, Kazutaka Matsuda, and Meng Wang. 2013. Enhancing Semantic Bidirectionalization via Shape Bidirectionalizer Plug-ins. Journal of Functional Programming 23, 5 (2013), 515–551.
35. Tao Zan, Li Liu, Hsiang-Shang Ko, and Zhenjiang Hu. 2016. Brul: A Putback-Based Bidirectional Transformation Library for Updatable Views. In International Workshop on Bidirectional Transformations (BX’16). CEUR-WS.org, 77–89. http: //ceur-ws.org/Vol-1571/paper_3.pdf
36. Weize Zhao, Haiyan Zhao, and Zhenjiang Hu. 2016. A Framework for Synchronization between Feature Configurations and Use Cases based on Bidirectional Programming. In International Model-Driven Requirements Engineering Workshop (MoDRE’16) . IEEE, 170–179.
37. Zirun Zhu, Yongzhe Zhang, Hsiang-Shang Ko, Pedro Martins, João Saraiva, and Zhenjiang Hu. 2016. Parsing and Reflective Printing, Bidirectionally. In International Conference on Software Language Engineering (SLE’16). ACM, 2–14.

Index Terms

• Software and its engineering

  • Software notations and tools

    • Context specific languages

      • Domain specific languages

• Theory of computation

  • Logic

    • Hoare logic

  • Semantics and reasoning

    • Program semantics

      • Axiomatic semantics