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).
Preview
Unable to display preview. Download preview PDF.
References
Date C. J. An Introduction to Database Systems, volume 1. Addison-Wesley, Reading, Massachusetts, USA, fifth edition, 1990.
Codd E. F. “A Relational Model of Data for Large Shared Data Banks”. Communications of the ACM, 13(6):377–387, June 1970.
Spivey J. M. The Z Notation: A Reference Manual. Prentice Hall International (UK) Ltd., Hemel Hempstead, UK, second edition, 1992.
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.
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.
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.
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.
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.
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.
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.
Barros R. S. M. “Company Database Example”. Department of Computing Science, The University of Glasgow, 1993. Third step specification.
American National Standards Institute. “The Database Language SQL”. Document ANSI X3.135, 1986.
J. A. Senn. The student version of dBASE IV, version 1.1 User's Manual. Addison-Wesley, Reading, Massachusetts, USA, 1991.
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.
Date C. J. Relational Database: Selected Writings. Addison-Wesley, Reading, Massachusetts, USA, 1986.
Date C. J. and White C. J. A Guide to DB2. Addison-Wesley, Reading, Massachusetts, USA, third edition, 1989.
J. M. Spivey. “A Guide to the zed Style Option”. Oxford University Computing Laboratory, 11 Keble Road, Oxford, UK, December 1990.
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.
Grammatech, Inc., Ithaca, NY, USA. The Synthesizer Generator Reference Manual, fourth edition, 1992.
Author information
Authors and Affiliations
Editor information
Rights 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