Article

Free access

Database theory for supporting specification-based database system development

Authors:

Tim SheardAuthors Info & Claims

ICSE '85: Proceedings of the 8th international conference on Software engineering

Pages 43 - 49

Published: 01 August 1985 Publication History

Abstract

We report on the development of a formal theory of databases designed to support specification-based development of database systems. This theory formalizes database systems which include non-first normal form relations, complex integrity constraints, transactions, and embedded data types such as integers, character strings, and user-defined types. Our theory is based on two axiomatized algebras (abstract data types) and is being used to mechanically prove the properties of relational algebra and functional dependencies, as well as the relationships between integrity constraints and the primitive operations on databases, e. g., inserts and deletes of tuples. We are also using the theory to prove whether or not specific transactions obey complex integrity constraints which can include universal and existential quantifiers. The latter proofs (as well as failed attempts at proofs) can be used during the design of specific systems and in the optimization of system implementations.

References

[1]

S. Gerhart, "Formal Validation of a Simple Database Application." Proceedings of the Sixteenth Hawaii International Conference on System Sciences, 1983, pp. 102-111.

[2]

R. BaIzer, T. E. Cheatham, Jr. and C. Green, "Software Technology in 1990's: Using a New Paradigm." Computer, Vol. 16, No. 16, November, 1983.

[3]

A. Walker and S. C. SaIveter, "Automatic Modification of Transactions to Preserve Data Base Integrity Without Undoing Updates." State University of New York, Stony Brook, New York: Tech. Report 8l/O26 (June 1981).

[4]

D. Stemple and T. Sheard, "Specification and Verification of Abstract Database Types", Proceedings of the Third ACM SIGACT-SIGMOD Symposium on Database Systems, Waterloo, Ontario, April, 1984, pp. 248-257.

Digital Library

[5]

P. P. Chen, "The Entity-Relationship Model - Toward a Unified View of Data." ACM Transactions on Database Systems, Vol. 1, No. 1, March, 1976, pp. 9-36.

Digital Library

[6]

J. M. Smith and D. C. P. Smith, "A Data Base Approach to Software Specification" In Software Development TOOIS, Riddle and Fairley, Eds., Springer-Verlag, 1980, pp. 176-204.

[7]

D. Stemple, "A Database Management Facility for Automatic Generation of Database Managers." ACM Transactions on Database Systems, vol. 1, no. 1, March 1976, pp. 79-94.

Digital Library

[8]

D. Stemple, "A Database Management Facility and Architecture for the Realization of Data Independence." Ph.D. thesis, Universtiy of Massachusetts at Amherst, February 1977.

Digital Library

[9]

H. Ehrig, H. J. Kreowski and H. Weber, "Algebraic Specification Schemes for Data Base Systems", Proceedings of the 4th International Conf. on Very Large Data Bases, 1978, pp. 427-444.

[10]

P. CLockemann, H. C. Mayr, W. H. WeiI and W. H. Wohleber, "Data Abstractions for Database Systems", ACM Trans. on Database Syst., Vol. 4, no. 4, March, 1978, pp. 30-59.

Digital Library

[11]

B. G. claybrook, "A Specification Method for Specifying Data and Procedural Abstractions", IEEE Transactions on Software Engineering, Vol. 8, no. 5, Sep., 1982, pp. 449459.

[12]

M. A. Casanova, P. A. S. Veloso and A. L. Furtado, "FormaI Data Base Specification - An Eclectic Perspective", Proceeding of the Third ACM SIGACT-SIGMOD Symposium on Database Systems, Waterloo, Ontario, April, 1984, pp. 110-118.

Digital Library

[13]

R. S. Boyer and J. S. Moore, A Computational Logic, Academic Press, New York, 1979.

[14]

G. Gardarin and M. Melkanoff, "Proving Consistency of Database Transactions", Proceeding of the 5th International Conf. on Very Large Databases, 1979, pp 291-298.

[15]

B. Liskov and S. Z&s, "Specification Techniques dor Data Abstractions", IEEE Transactions on Software Engineering, Vol 1, no. 1, March, 1975, pp. 7-19.

Digital Library

[16]

C. Beeri, P. A. Bernstein and N. Goodman, "A Sophisticate's Introduction to Database Normalization", Proceedings of the Fourth International Conference on Very Large Databases, West Berlin, Germany, Sep., 1978, pp. 113-124.

[17]

P. A. Bernstein and B. T. Blaustein, "Fast Methods for Testing Quantified Relational CaIcuIus Expressions", Proceedings of 1982 ACM SIGMOD Conference, pp. 39-50.

Digital Library

[18]

R. M. Burstah and J. A. Goguen, "Putting Theories together to Make Specifications." Fifth International Joint Conference on Artificial Intelligence, Cambridge, Massachusetts, August, 1977, pp. 1045-1058.

[19]

J. A. Goguen and R. M. Burstah, "Introducing Institutions." in L.ecture Notes in Computer Science 164, bgics of Programs, E. Clarke and D. Kozen, Eds., Springer Verlag, Be&, 1983.

Digital Library

[20]

J. M. Nicolas, "Logic for Improving Integrity Checking in Relational Data Bases", Acta Informatica, Vol. 18, no. 3, Dec., 1982, pp. 227-254.

Cited By

Sheard TStemple D(1989)Automatic verification of database transaction safetyACM Transactions on Database Systems10.1145/68012.6801414:3(322-368)Online publication date: 1-Sep-1989
https://dl.acm.org/doi/10.1145/68012.68014
Mazumdar SStemple DSheard T(1988)Resolving the tension between integrity and security using a theorem proverACM SIGMOD Record10.1145/971701.5023117:3(233-242)Online publication date: 1-Jun-1988
https://dl.acm.org/doi/10.1145/971701.50231
Mazumdar SStemple DSheard T(1988)Resolving the tension between integrity and security using a theorem proverProceedings of the 1988 ACM SIGMOD international conference on Management of data10.1145/50202.50231(233-242)Online publication date: 1-Jun-1988
https://dl.acm.org/doi/10.1145/50202.50231
Show More Cited By

Index Terms

Database theory for supporting specification-based database system development
1. Social and professional topics
  1. Professional topics
    1. Management of computing and information systems
      1. Project and people management
2. Software and its engineering
  1. Software creation and management
    1. Designing software
      1. Requirements analysis
    2. Software development process management
  2. Software notations and tools
    1. Software configuration management and version control systems

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICSE '85: Proceedings of the 8th international conference on Software engineering

August 1985

402 pages

ISBN:0818606207

Chairmen:
Meir M. Lehman,
Horst Hünke
Commission of European Communities, Brussels, Belgium
,
Barry Boehm
TRW-DSG, Redondo, CA

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering
IEEE-CS: Computer Society

Publisher

IEEE Computer Society Press

Washington, DC, United States

Publication History

Published: 01 August 1985

Check for updates

Qualifiers

Article

Acceptance Rates

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
290
Total Downloads

Downloads (Last 12 months)58
Downloads (Last 6 weeks)12

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Sheard TStemple D(1989)Automatic verification of database transaction safetyACM Transactions on Database Systems10.1145/68012.6801414:3(322-368)Online publication date: 1-Sep-1989
https://dl.acm.org/doi/10.1145/68012.68014
Mazumdar SStemple DSheard T(1988)Resolving the tension between integrity and security using a theorem proverACM SIGMOD Record10.1145/971701.5023117:3(233-242)Online publication date: 1-Jun-1988
https://dl.acm.org/doi/10.1145/971701.50231
Mazumdar SStemple DSheard T(1988)Resolving the tension between integrity and security using a theorem proverProceedings of the 1988 ACM SIGMOD international conference on Management of data10.1145/50202.50231(233-242)Online publication date: 1-Jun-1988
https://dl.acm.org/doi/10.1145/50202.50231
Stemple DMazumdar SSheard T(1987)On the modes and meaning of feedback to transaction designersACM SIGMOD Record10.1145/38714.3875316:3(374-386)Online publication date: 1-Dec-1987
https://dl.acm.org/doi/10.1145/38714.38753
Stemple DMazumdar SSheard T(1987)On the modes and meaning of feedback to transaction designersProceedings of the 1987 ACM SIGMOD international conference on Management of data10.1145/38713.38753(374-386)Online publication date: 1-Dec-1987
https://dl.acm.org/doi/10.1145/38713.38753

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents