Specification and Verification of Abstract Database Types.

David W. Stemple, Tim Sheard: Specification and Verification of Abstract Database Types. PODS 1984: 248-257
  author    = {David W. Stemple and
               Tim Sheard},
  title     = {Specification and Verification of Abstract Database Types},
  booktitle = {Proceedings of the Third ACM SIGACT-SIGMOD Symposium on Principles
               of Database Systems, April 2-4, 1984, Waterloo, Ontario, Canada},
  publisher = {ACM},
  year      = {1984},
  isbn      = {0-89791-128-8},
  pages     = {248-257},
  ee        = {, db/conf/pods/StempleS84.html},
  crossref  = {DBLP:conf/pods/84},
  bibsource = {DBLP,}


A database system, comprising a schema, integrity constraints, transactions, and queries, constitutes a single abstract data type. This type, which we call an abstract database type, has as its object the database itself. Thus, the value set of such a type is the set of all legal database states, legal in the sense of obeying all the structural specifications of the schema and the semantic prescriptions of the integrity constraints. The database transactions are the operations of the abstract database type and must be functions on the value set of the type. A transaction specification is safe if it defines a function which is closed on the database state set, i. e., any execution of the transaction on a legal database yields a legal database.

We propose an approach to the definition of abstract database types which is both usable by typical database designers and which facilitates the mechanical verification of transaction safety. The Boyer and Moore theorem proving technique is used to prove transaction safety theorems using abstract data type axioms and recursive functions generated from the database schema and transaction program.

Copyright © 1984 by the ACM, Inc., used by permission. Permission to make digital or hard copies is granted provided that copies are not made or distributed for profit or direct commercial advantage, and that copies show this notice on the first page or initial screen of a display along with the full citation.

Load The ACM SIGMOD Anthology, CDROM Edition, Volume 1-3, PODS '82-'98. and ... Load The ACM SIGMOD Anthology, Silver Edition, DVD 1, Proceedings. and ... BibTeX

Printed Edition

Proceedings of the Third ACM SIGACT-SIGMOD Symposium on Principles of Database Systems, April 2-4, 1984, Waterloo, Ontario, Canada. ACM 1984, ISBN 0-89791-128-8
Contents BibTeX

Online Edition: ACM Digital Library


Philip A. Bernstein, Barbara T. Blaustein, Edmund M. Clarke: Fast Maintenance of Semantic Integrity Assertions Using Redundant Aggregate Data. VLDB 1980: 126-136 BibTeX
Philip A. Bernstein, Barbara T. Blaustein: Fast Methods for Testing Quantified Relational Calculus Assertions. SIGMOD Conference 1982: 39-50 BibTeX
Michael L. Brodie: The application of data types to database semantic integrity. Inf. Syst. 5(4): 287-296(1980) BibTeX
Michael L. Brodie: Association: A Database Abstraction for Semantic Modelling. ER 1981: 577-602 BibTeX
Peter Buneman, Eric K. Clemons: Efficient Monitoring Relational Databases. ACM Trans. Database Syst. 4(3): 368-382(1979) BibTeX
Billy G. Claybrook: A Specification Method for Specifying Data and Procedural Abstractions. IEEE Trans. Software Eng. 8(5): 449-459(1982) BibTeX
Hartmut Ehrig, Hans-Jörg Kreowski, Herbert Weber: Algebraic Specification Schemes for Data Base Systems. VLDB 1978: 427-440 BibTeX
Georges Gardarin, Michel A. Melkanoff: Proving Consistency of Database Transactions. VLDB 1979: 291-298 BibTeX
Michael Hammer, Sunil K. Sarin: Efficient Monitoring of Database Assertions (Abstract). SIGMOD Conference 1978: 159 BibTeX
C. A. R. Hoare: An Axiomatic Basis for Computer Programming. Commun. ACM 12(10): 576-580(1969) BibTeX
Peter C. Lockemann, Heinrich C. Mayr, Wolfgang H. Weil, Wolfgang H. Wohlleber: Data Abstractions for Database Systems. ACM Trans. Database Syst. 4(1): 60-75(1979) BibTeX
Zohar Manna, Jean Vuillemin: Fix Point Approach to the Theory of Computation. Commun. ACM 15(7): 528-536(1972) BibTeX
Jean-Marie Nicolas: Logic for Improving Integrity Checking in Relational Data Bases. Acta Inf. 18: 227-253(1982) BibTeX
Clesio Saraiva dos Santos, Erich J. Neuhold, Antonio L. Furtado: A Data Type Approach to the Entity-Relationship Approach. ER 1979: 103-119 BibTeX
Peter Scheuermann, Gerd Schiffner, H. Weber: Abstraction Capabilities and Invariant Properties Modelling within the Entity-Relationship Approach. ER 1979: 121-140 BibTeX
Joachim W. Schmidt: Some High Level Language Constructs for Data of Type Relation. ACM Trans. Database Syst. 2(3): 247-261(1977) BibTeX
Herbert Weber: A Software Engineering View of Data Base Systems. VLDB 1978: 36-51 BibTeX
Raymond T. Yeh, Jerry W. Baker: Toward a Design Methodology for DBMS: A Software Engineering Approach. VLDB 1977: 16-27 BibTeX

Referenced by

  1. Subhasish Mazumdar, David W. Stemple: Helping the Database Designer Maintain Inegrity Constraints. IEEE Data Eng. Bull. 17(2): 28-32(1994)
  2. Lissa F. Pollacia, Lois M. L. Delcambre: The Object Flow Model: A Formal Framework for Describing the Dynamic Construction, Destruction and Interaction of Complex Objects. ER 1993: 1-12
  3. Subhasish Mazumdar: Optimizing Distributed Integrity Constraints. DASFAA 1993: 327-334
  4. Tim Sheard, David W. Stemple: Automatic Verification of Database Transaction Safety. ACM Trans. Database Syst. 14(3): 322-368(1989)
  5. Alexander Borgida, John Mylopoulos, Joachim W. Schmidt, Ingrid Wetzel: Support for Data-Intensive Applications: Conceptual Design and Software Development. DBPL 1989: 258-280
  6. Udo W. Lipeck: Transformation of Dynamic Integrity Constraints into Transaction Specifications. ICDT 1988: 322-337
  7. David W. Stemple, Subhasish Mazumdar, Tim Sheard: On the Modes and Meaning of Feedback to Transaction Designers. SIGMOD Conference 1987: 374-386
  8. David W. Stemple, Tim Sheard, Ralph E. Bunker: Abstract Data Types in Databases: Specification, Manipulation and Access. ICDE 1986: 590-597
  9. Tim Sheard, David W. Stemple: Coping with Complexity in Automated Reasoning about Database Systems. VLDB 1985: 426-435
ACM SIGMOD Anthology - DBLP: [Home | Search: Author, Title | Conferences | Journals]
ACM SIGMOD Anthology: Copyright © by ACM (, Corrections:
DBLP: Copyright © by Michael Ley (, last change: Sat May 16 23:33:45 2009