Abstract
We constructed a tool, called VooDooM, which converts datatypes in Vdm-sl into Sql relational data models. The conversion involves transformation of algebraic types to maps and products, and pointer introduction.
The conversion is specified as a theory of refinement by calculation. The implementation technology is strategic term rewriting in Haskell, as supported by the Strafunski bundle. Due to these choices of theory and technology, the road from theory to practise is straightforward.
This is a preview of subscription content, log in via an institution to check access.
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
Almeida, J.J., Barbosa, L.S., Neves, F.L., Oliveira, J.N.: Bringing Camila and SetCalc Together — the bams.cam and ppd.cam Camila Toolset demos. Technical report, DI/UM, Braga(December 1997) [45 p. doc.]
Alves, T., Visser, J.: Development of an industrial strength grammar for VDM. Technical Report DI-PURe-05.04.29, Universidade do Minho (2005)
Backhouse, R.C., de Bruin, P., Hoogendijk, P., Malcolm, G., Voermans, T.S., van der Woude, J.: Polynomial relators. In: Kim, K.-c. (ed.) PKC 2001. LNCS, vol. 1992, pp. 303–362. Springer, Heidelberg (2001)
Baluta, D.D.: A formal specification in Z of the relational data model, Version 2, of E.F. Codd. M. Sc. thesis, Concordia University, Montreal, QC, Canada (1995)
de Barros, R.S.M.: Deriving relational database programs from formal specifications. In: Naftalin, M., Bertrán, M., Denvir, T. (eds.) FME 1994. LNCS, vol. 873, pp. 703–723. Springer, Heidelberg (1994)
Bjorner, D., Jones, C.B.: Formal Specification and Software Development. In: Hoare, C.A.R. (ed.). Series in Computer Science, Prentice-Hall International, Englewood Cliffs (1982)
Cirstea, H., Kirchner, C., Liquori, L.: The Rho Cube. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol. 2030, pp. 168–180. Springer, Heidelberg (2001)
Codd, E.F.: Missing Information. Addison-Wesley Publishing Company, Inc., Reading (1990)
Codd, E.F.: A relational model of data for large shared data banks. Communications of the ACM 13(6), 377–387 (1970)
Fitzgerald, J., Larsen, P.G.: Modelling Systems: Practical Tools and Techniques for Software Development, 1st edn. Cambridge University Press, Cambridge (1998)
Fitzgerald, J.S., Jones, C.B.: Modularizing the formal description of a database system. In: Langmaack, H., Hoare, C.A.R., Bjorner, D. (eds.) VDM 1990. LNCS, vol. 428. Springer, Heidelberg (1990)
Garcia-Molina, H., Ullman, J.D., Widom, J.D.: Database Systems: The Complete Book. Prentice Hall, Englewood Cliffs (2002); ISBN: 0-13-031995-3
Hoogendijk, P.: A Generic Theory of Data Types. PhD thesis, University of Eindhoven, The Netherlands (1997)
Hutton, G., Wright, J.: Compiling exceptions correctly. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 211–227. Springer, Heidelberg (2004)
ISO. Information technology — programmming languages, their environments and system software interfaces — Vienna Development Method — specification language — part 1: Base language (December 1996) (ISO/IEC 13817-1, Geneva)
ISO. Information Technology – Database languages – SQL. Reference number ISO/IEC 9075:1992(E) (November 1992)
Jones, C.B.: Software Development — A Rigorous Approach. In: Hoare, C.A.R. (ed.) Series in Computer Science, Prentice-Hall International, Englewood Cliffs (1980)
de Jonge, M., Visser, J.: Grammers as contracts. In: Butler, G., Jarzabek, S. (eds.) GCSE 2000. LNCS, vol. 2177, pp. 85–99. Springer, Heidelberg (2001)
Kuipers, T., Visser, J.: Object-oriented tree traversal with JJForester. In: van den Brand, M., Parigot, D. (eds.) Proc. Workshop on Language Descriptions, Tools and Applications. Electronic Notes in Theoretical Computer Science, vol. 44, Elsevier Science, Amsterdam (2001)
Lämmel, R.: Typed Generic Traversal With Term Rewriting Strategies. Journal of Logic and Algebraic Programming 54 (2003)
Lämmel, R., Peyton Jones, S.: Scrap your boilerplate: a practical design pattern for generic programming. ACM SIGPLAN Notices 38(3), 26–37 (2003); Proc. ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI 2003)
Lämmel, R., Visser, J.: Strategic polymorphism requires just two combinators! Technical Report cs.PL/0212048, arXiv (December 2002)
Lämmel, R., Visser, J.: A Strafunski application letter. In: Dahl, V., Wadler, P. (eds.) PADL 2003. LNCS, vol. 2562, pp. 357–375. Springer, Heidelberg (2002)
Maier, D.: The Theory of Relational Databases. Computer Science Press, Rockville (1983)
Morgan, C.: Programming from Specification. In: Hoare, C.A.R. (ed.) Series in Computer Science, Prentice-Hall International, Englewood Cliffs (1990)
Necco, C.: Polytypic data processing. Master’s thesis, Facultad de Cs. Físico Matemáticas y Naturales, University of San Luis, Argentina (submitted, 2005)
Neves, F.L., Oliveira, J.N.: ART — Um Laborat=rio de Reificatpo ”GenTtica”. In: IBERAMIA 1998 — Sixth Ibero-Conference on Artificial Intelligence, Lisbon, Portugal, October 5-9, 1998, pp. 201–215 (1998) (in Portuguese)
Neves, F.L., Silva, J.C., Oliveira, J.N.: Converting Informal Meta-data to VDM-SL: A Reverse Calculation Approach. In: VDM in Practice! A Workshop co-located with FM 1999: The World Congress on Formal Methods, Toulouse, France (September 1999)
Oliveira, J.N.: A reification calculus for model-oriented software specification. Formal Aspects of Computing 2(1), 1–23 (1990)
Oliveira, J.N.: 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, January 8–10, 1992, pp. 140–171. Springer, London, UK (1992) (invited paper); ISBN 0387197524
Oliveira, J.N.: Data processing by calculation, 2001. In: Lecture Notes for the 6th Estonian Winter School in Computer Science, Palmse, Estonia, March 4-9, 2001, pages 108 (2001)
Oliveira, J.N.: Calculate databases with ‘simplicity’, Presentation at the IFIP WG 2.1 #59 Meeting, Nottingham, UK (September 2004)
Samson, W.B., Wakelin, A.W.: Algebraic Specification of Databases: A Survey from a Database Perspective. In: Workshops in Computing. Springer, Glasgow (1992)
Ullman, J.D.: Principles of Database and Knowledge-Base Systems. Computer Science Press, Rockville (1988)
Visser, E., Benaissa, Z.: A Core Language for Rewriting. In: Kirchner, C., Kirchner, H. (eds.) Proc. International Workshop on Rewriting Logic and its Applications (WRLA 1998), Pont-à-Mousson, France, September 1998. ENTCS, vol. 15, Elsevier Science, Amsterdam (1998)
Visser, J.: Visitor combination and traversal control. ACM SIGPLAN Notices 36(11), 270–282 (2001); Proceedings of the ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2001)
Wagner, E.G.: All recursive types defined using products and sums can be implemented using pointers. In: Bergman, C.H., Pigozzi, D.L., Maddux, R.D. (eds.) Algebraic Logic and Universal Algebra in Computer Science. LNCS, vol. 425. Springer, Heidelberg (1990)
Walshe, A.: NDB: The Formal Specification and Rigorous Design of a Single-User Database System. Prentice Hall, Englewood Cliffs (1990); ISBN 0-13-116088-5
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alves, T.L., Silva, P.F., Visser, J., Oliveira, J.N. (2005). Strategic Term Rewriting and Its Application to a Vdm-sl to Sql Conversion. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds) FM 2005: Formal Methods. FM 2005. Lecture Notes in Computer Science, vol 3582. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11526841_27
Download citation
DOI: https://doi.org/10.1007/11526841_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27882-5
Online ISBN: 978-3-540-31714-2
eBook Packages: Computer ScienceComputer Science (R0)