Skip to main content

Deriving relational database programs from formal specifications

  • Papers
  • Conference paper
  • First Online:
FME '94: Industrial Benefit of Formal Methods (FME 1994)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 873))

Included in the following conference series:

Abstract

The derivation of database programs directly from formal specifications is a well known and unsolved problem. Most of the previous work on the area either tried to solve the problem too generally or was restricted to some trivial aspects, for example deriving the database structure and/or simple operations. However difficult in general, deriving relational database applications directly from Z specifications satisfying a certain set of rules (the method) is not arduous. This paper describes a set of rules on how to map such specifications to database programs. If appropriate tool support is provided, writing formal specifications according to the method and deriving the corresponding relational database programs should be straightforward. Moreover it should produce code which is standardized and thus easier to understand and maintain.

The author is a Brazilian Civil Servant, sponsored by CAPES, on leave from Federal University of Pernambuco (UFPE).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Date C. J. An Introduction to Database Systems, volume 1. Addison-Wesley, Reading, Massachusetts, USA, fifth edition, 1990.

    Google Scholar 

  2. Codd E. F. “A Relational Model of Data for Large Shared Data Banks”. Communications of the ACM, 13(6):377–387, June 1970.

    Google Scholar 

  3. Spivey J. M. The Z Notation: A Reference Manual. Prentice Hall International (UK) Ltd., Hemel Hempstead, UK, second edition, 1992.

    Google Scholar 

  4. Potter B. F., Sinclair J. E., and Till D. An Introduction to Formal Specification and Z. Prentice Hall International (UK) Ltd., Hemel Hempstead, UK, 1991.

    Google Scholar 

  5. Barros R. S. M. and Harper D. J. “A Method for the Specification of Relational Database Applications”. In Nicholls J. E. (ed.), Z User Workshop, York 1991, Workshops in Computing series, pages 261–286. Springer-Verlag, 1992.

    Google Scholar 

  6. Barros R. S. M. “Formal Specification of Relational Database Applications: A Method and an Example”. Research report GE-93-02, Department of Computing Science, The University of Glasgow, September 1993.

    Google Scholar 

  7. Barros R. S. M. On the Formal Specification and Derivation of Relational Database Applications. PhD thesis, The University of Glasgow, Department of Computing Science, 1994. In preparation.

    Google Scholar 

  8. Barros R. S. M. “On the Derivation of Relational Database Programs from Formal Specifications”. Research report, Department of Computing Science, The University of Glasgow, 1994.

    Google Scholar 

  9. Schmidt J. W. and Matthes F. “The Database Programming Language DBPL: Rationale and Report”. FIDE technical report FIDE/92/46, Universität Hamburg, Germany, 1992.

    Google Scholar 

  10. Matthes F., Rudloff A., Schmidt J. W., and Subieta K. “The Database Programming Language DBPL: User and System Manual”. FIDE technical report FIDE/92/47, Universität Hamburg, Germany, 1992.

    Google Scholar 

  11. Barros R. S. M. “Company Database Example”. Department of Computing Science, The University of Glasgow, 1993. Third step specification.

    Google Scholar 

  12. American National Standards Institute. “The Database Language SQL”. Document ANSI X3.135, 1986.

    Google Scholar 

  13. J. A. Senn. The student version of dBASE IV, version 1.1 User's Manual. Addison-Wesley, Reading, Massachusetts, USA, 1991.

    Google Scholar 

  14. van Diepen M. J. and van Hee K. M. “A Formal Semantics for Z and the link between Z and the Relational Algebra”. In Bjørner D., Hoare C. A. R., and Langmaack H. (eds.), VDM and Z — Formal Methods in Software Development, volume 428 of Lecture Notes in Computing Science, pages 526–551. Springer-Verlag, 1990.

    Google Scholar 

  15. Date C. J. Relational Database: Selected Writings. Addison-Wesley, Reading, Massachusetts, USA, 1986.

    Google Scholar 

  16. Date C. J. and White C. J. A Guide to DB2. Addison-Wesley, Reading, Massachusetts, USA, third edition, 1989.

    Google Scholar 

  17. J. M. Spivey. “A Guide to the zed Style Option”. Oxford University Computing Laboratory, 11 Keble Road, Oxford, UK, December 1990.

    Google Scholar 

  18. Reps T. W. and Teitelbaum T. The Synthesizer Generator: a system for constructing language-based editors. Texts and monographs in computer science. Springer-Verlag, New York, USA, 1989.

    Google Scholar 

  19. Grammatech, Inc., Ithaca, NY, USA. The Synthesizer Generator Reference Manual, fourth edition, 1992.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Maurice Naftalin Tim Denvir Miquel Bertran

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

de Barros, R.S.M. (1994). Deriving relational database programs from formal specifications. In: Naftalin, M., Denvir, T., Bertran, M. (eds) FME '94: Industrial Benefit of Formal Methods. FME 1994. Lecture Notes in Computer Science, vol 873. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58555-9_123

Download citation

  • DOI: https://doi.org/10.1007/3-540-58555-9_123

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58555-8

  • Online ISBN: 978-3-540-49031-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics