This paper addresses the foundations of data-model transformation. A catalog of data mappings is presented which includes abstraction and representation relations and associated constraints. These are justified in an algebraic style via the pointfree-transform, a technique whereby predicates are lifted to binary relation terms (of the algebra of programming) in a two-level style encompassing both data and operations. This approach to data calculation, which also includes transformation of recursive data models into “flat” database schemes, is offered as alternative to standard database design from abstract models. The calculus is also used to establish a link between the proposed transformational style and bidirectional lenses developed in the context of the classical view-update problem.


Theoretical foundations mapping scenarios transformational design refinement by calculation 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Aarts, C., Backhouse, R.C., Hoogendijk, P., Voermans, E., van der Woude, J.: A relational theory of datatypes (December 1992),
  2. 2.
    Alves, T.L., Silva, P.F., Visser, J., Oliveira, J.N.: Strategic term rewriting and its application to a VDM-SL to SQL conversion. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 399–414. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  3. 3.
    Ambler, S.W.: The object-relational impedance mismatch (February15, 2006),
  4. 4.
    Backhouse, K., Backhouse, R.C.: Safety of abstract interpretations for free, via logical relations and Galois connections. SCP 15(1–2), 153–196 (2004)MathSciNetzbMATHGoogle Scholar
  5. 5.
    Backhouse, R.C.: Mathematics of Program Construction, pages 608. Univ. of Nottingham (2004); Draft of book in preparationGoogle Scholar
  6. 6.
    Backhouse, R.C., de Bruin, P., Hoogendijk, P., Malcolm, G., Voermans, T.S., van der Woude, J.: Polynomial relators. In: AMAST 1991, pp. 303–362. Springer, Heidelberg (1992)Google Scholar
  7. 7.
    Backus, J.: Can programming be liberated from the von Neumann style? a functional style and its algebra of programs. CACM 21(8), 613–639 (1978)CrossRefMathSciNetzbMATHGoogle Scholar
  8. 8.
    Barbosa, L.S., Oliveira, J.N., Silva, A.M.: Calculating invariants as coreflexive bisimulations. In: Meseguer, J., Roşu, G. (eds.) AMAST 2008. LNCS, vol. 5140, pp. 83–99. Springer, Heidelberg (2008)Google Scholar
  9. 9.
    Berdaguer, P.: Algebraic representation of UML class-diagrams, May, Dept. Informatics, U.Minho. Technical note (2007)Google Scholar
  10. 10.
    Berdaguer, P., Cunha, A., Pacheco, H., Visser, J.: Coupled Schema Transformation and Data Conversion For XML and SQL. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 290–304. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  11. 11.
    Bird, R., de Moor, O.: Algebra of Programming. C.A.R. Hoare, series editor, Series in Computer Science. Prentice-Hall International, Englewood Cliffs (1997)zbMATHGoogle Scholar
  12. 12.
    Bird, R.S.: Unfolding pointer algorithms. J. Funct. Program. 11(3), 347–358 (2001)CrossRefzbMATHGoogle Scholar
  13. 13.
    Bohannon, A., Foster, J.N., Pierce, B.C., Pilkiewicz, A., Schmitt, A.: Boomerang: Resourceful lenses for string data. In: ACM SIGPLAN–SIGACT POPL Symposium, pp. 407–419 (January 2008)Google Scholar
  14. 14.
    Bohannon, A., Vaughan, J.A., Pierce, B.C.: Relational lenses: A language for updateable views. In: Principles of Database Systems (PODS) (2006)Google Scholar
  15. 15.
    Booch, G., Rumbaugh, J., Jacobson, I.: The Unified Modeling Language User Guide. Addison-Wesley Longman, Amsterdam (1999)Google Scholar
  16. 16.
    Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. JACM 24(1), 44–67 (1977)CrossRefMathSciNetzbMATHGoogle Scholar
  17. 17.
    Cunha, A., Oliveira, J.N., Visser, J.: Type-safe two-level data transformation. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 284–289. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  18. 18.
    Cunha, A., Visser, J.: Transformation of structure-shy programs: applied to XPath queries and strategic functions. In: PEPM 2007, pp. 11–20. ACM, New York (2007)Google Scholar
  19. 19.
    Darlington, J.: A synthesis of several sorting algorithms. Acta Informatica 11, 1–30 (1978)CrossRefMathSciNetzbMATHGoogle Scholar
  20. 20.
    de Roever, W.-P., Engelhardt, K., Coenen, J., Buth, K.-H., Gardiner, P., Lakhnech, Y., Stomp, F.: Data Refinement Model-Oriented Proof methods and their Comparison. Cambridge University Press, Cambridge (1999)Google Scholar
  21. 21.
    Deutsch, M., Henson, M., Reeves, S.: Modular reasoning in Z: scrutinising monotonicity and refinement (to appear, 2006)Google Scholar
  22. 22.
    Dijkman, R.M., Pires, L.F., Joosten, S.: Calculating with concepts: a technique for the development of business process support. In: pUML. LNI, vol. 7, pp. 87–98. GI (2001)Google Scholar
  23. 23.
    Doornbos, H., Backhouse, R., van der Woude, J.: A calculational approach to mathematical induction. Theoretical Computer Science 179(1–2), 103–135 (1997)CrossRefMathSciNetzbMATHGoogle Scholar
  24. 24.
    Fielding, E.: The specification of abstract mappings and their implementation as B + -trees. Technical Report PRG-18, Oxford University (September 1980)Google Scholar
  25. 25.
    Fitzgerald, J., Larsen, P.G.: Modelling Systems: Practical Tools and Techniques for Software Development, 1st edn. Cambridge University Press, Cambridge (1998)zbMATHGoogle Scholar
  26. 26.
    Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J.T. (ed.) Proc. Symposia in Applied Mathematics Mathematical Aspects of Computer Science, vol. 19, pp. 19–32. American Mathematical Society (1967)Google Scholar
  27. 27.
    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 Trans. Program. Lang. Syst 29(3), 17 (2007)CrossRefzbMATHGoogle Scholar
  28. 28.
    Frias, M.F.: Fork algebras in algebra, logic and computer science. Logic and Computer Science. World Scientific Publishing Co, Singapore (2002)CrossRefzbMATHGoogle Scholar
  29. 29.
    Gibbons, J.: When is a function a fold or an unfold?, Working document 833 FAV-12 available from the website of IFIP WG 2.1, 57th meeting, New York City, USA (2003)Google Scholar
  30. 30.
    Hainaut, J.-L.: The transformational approach to database engineering. In: Lämmel, R., Saraiva, J., Visser, J. (eds.) GTTSE 2005. LNCS, vol. 4143, pp. 95–143. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  31. 31.
    He, J., Hoare, C.A.R., Sanders, J.W.: Data refinement refined. In: Robinet, B., Wilhelm, R. (eds.) ESOP 1986. LNCS, vol. 213, pp. 187–196 (1986)Google Scholar
  32. 32.
    Hoogendijk, P.: A Generic Theory of Data Types. PhD thesis, University of Eindhoven, The Netherlands (1997)Google Scholar
  33. 33.
    Hu, Z., Mu, S.-C., Takeichi, M.: A programmable editor for developing structured documents based on bidirectional transformations. In: Proc. ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, pp. 178–189. ACM Press, New York (2004)Google Scholar
  34. 34.
    Hutton, G., Meijer, E.: Back to basics: Deriving representation changers functionally. Journal of Functional Programming (1993) (Functional Pearl)Google Scholar
  35. 35.
    Hutton, G., Wright, J.: Compiling exceptions correctly. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 211–227. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  36. 36.
    Jackson, D.: Software abstractions: logic, language, and analysis. The MIT Press, Cambridge Mass (2006)Google Scholar
  37. 37.
    Jeuring, J., Jansson, P.: Polytypic programming. In: Advanced Functional Programming. Springer, Heidelberg (1996)Google Scholar
  38. 38.
    Jones, C.B.: Systematic Software Development Using VDM, 1st edn. Series in Computer Science. Prentice-Hall Int., Englewood Cliffs (1986)zbMATHGoogle Scholar
  39. 39.
    Jourdan, I.S.: Reificação de tipos abstractos de dados: Uma abordagem matemática. Master’s thesis, University of Coimbra (1992) (in Portuguese)Google Scholar
  40. 40.
    Kahl, W.: Refinement and development of programs from relational specifications. ENTCS 4, 1–4 (2003)Google Scholar
  41. 41.
    Kreyszig, E.: Advanced Engineering Mathematics, 6th edn. J. Wiley & Sons, Chichester (1988)zbMATHGoogle Scholar
  42. 42.
    Lämmel, R., Meijer, E.: Mappings make data processing go round. In: Lämmel, R., Saraiva, J., Visser, J. (eds.) GTTSE 2005. LNCS, vol. 4143, pp. 169–218. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  43. 43.
    Lano, K.: Catalogue of model transformations,
  44. 44.
    Lawvere, B., Schanuel, S.: Conceptual Mathematics: a First Introduction to Categories. Cambridge University Press, Cambridge (1997)zbMATHGoogle Scholar
  45. 45.
    Maier, D.: The Theory of Relational Databases. Computer Science Press (1983)Google Scholar
  46. 46.
    McCarthy, J.: Towards a mathematical science of computation. In: Popplewell, C.M. (ed.) Proc. IFIP 62, pp. 21–28. North-Holland Pub.Company, Amsterdam (1963)Google Scholar
  47. 47.
    McLarty, C.: Elementary Categories, Elementary Toposes, 1st edn. Oxford Logic Guides, vol. 21. Calendron Press, Oxford (1995)zbMATHGoogle Scholar
  48. 48.
    Meng, S., Barbosa, L.S.: On refinement of generic state-based software components. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 506–520. Springer, Heidelberg (2004) (Best student co-authored paper award)CrossRefGoogle Scholar
  49. 49.
    Morgan, C.: Programming from Specification. C.A.R. Hoare, series (ed.), Series in Computer Science. Prentice-Hall International, Englewood Cliffs (1990)Google Scholar
  50. 50.
    Necco, C., Oliveira, J.N., Visser, J.: Extended static checking by strategic rewriting of pointfree relational expressions. Technical Report FAST:07.01, CCTC Research Centre, University of Minho (2007)Google Scholar
  51. 51.
    Oliveira, J.N.: Refinamento transformacional de especificaşões (terminais). In: Proc. of XII Jornadas Luso-Espanholas de Matemática, vol. II, pp. 412–417 (May 1987)Google Scholar
  52. 52.
    Oliveira, J.N.: A Reification Calculus for Model-Oriented Software Specification. Formal Aspects of Computing 2(1), 1–23 (1990)CrossRefzbMATHGoogle Scholar
  53. 53.
    Oliveira, J.N.: Invited paper: Software Reification using the SETS Calculus. In: Denvir, T., Jones, C.B., Shaw, R.C. (eds.) Proc. of the BCS FACS 5th Refinement Workshop, Theory and Practice of Formal Software Development, London, UK, pp. 140–171. Springer, Heidelberg (1992)Google Scholar
  54. 54.
    Oliveira, J.N.: Data processing by calculation. In: 6th Estonian Winter School in Computer Science, Palmse, Estonia, March 4-9, 2001. Lecture notes, pages 108 (2001)Google Scholar
  55. 55.
    Oliveira, J.N.: Constrained datatypes, invariants and business rules: a relational approach, PUReCafé, DI-UM, 2004.5.20 [talk], PURE Project (POSI/CHS/44304/2002) (2004)Google Scholar
  56. 56.
    Oliveira, J.N.: Calculate databases with simplicity, Presentation at the IFIP WG 2.1 #59 Meeting, Nottingham, UK (September 2004) (Slides available from the author’s website)Google Scholar
  57. 57.
    Oliveira, J.N.: Reinvigorating pen-and-paper proofs in VDM: the pointfree approach. In: The Third OVERTURE Workshop, Newcastle, UK, 27-28 November (2006)Google Scholar
  58. 58.
    Oliveira, J.N.: Pointfree foundations for (generic) lossless decomposition (submitted, 2007)Google Scholar
  59. 59.
    Oliveira, J.N., Rodrigues, C.J.: Transposing relations: from Maybe functions to hash tables. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 334–356. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  60. 60.
    Oliveira, J.N., Rodrigues, C.J.: Pointfree factorization of operation refinement. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085. pp. 236–251. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  61. 61.
    Pratt, V.: Origins of the calculus of binary relations. In: Proc. of the 7th Annual IEEE Symp. on Logic in Computer Science, pp. 248–254. IEEE Computer Society Press, Los Alamitos (1992)Google Scholar
  62. 62.
    Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55–74 (2002)Google Scholar
  63. 63.
    Rodrigues, C.J.: Software Refinement by Calculation. PhD thesis, Departamento de Informática, Universidade do Minho (submitted, 2007)Google Scholar
  64. 64.
    Wang, S., Barbosa, L.S., Oliveira, J.N.: A relational model for confined separation logic. In: TASE 2008, The 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering, June 17 - 19. LNCS. Springer, Heidelberg (2008)Google Scholar
  65. 65.
    Sestoft, P.: Deriving a lazy abstract machine. J. Funct. Program 7(3), 231–264 (1997)CrossRefMathSciNetzbMATHGoogle Scholar
  66. 66.
    Sheard, T., Pasalic, E.: Two-level types and parameterized modules. Journal of Functional Programming 14(5), 547–587 (2004)CrossRefzbMATHGoogle Scholar
  67. 67.
    Thomas, D.: The impedance imperative tuples + objects + infosets =too much stuff! Journal of Object Technology 2(5) (September/ October 5, 2003)Google Scholar
  68. 68.
    Visser, J.: Generic Traversal over Typed Source Code Representations. Ph. D. dissertation, University of Amsterdam, Amsterdam, The Netherlands (2003)Google Scholar
  69. 69.
    Wagner, E.G.: All recursive types defined using products and sums can be implemented using pointers. In: Bergman, C., Maddux, R.D., Pigozzi, D. (eds.) Algebraic Logic and Universal Algebra in Computer Science. LNCS, vol. 425. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  70. 70.
    Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice-Hall, Inc., Upper Saddle River (1996)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • José N. Oliveira
    • 1
  1. 1.CCTCUniversidade do MinhoBragaPortugal

Personalised recommendations