Specification and Verification of Abstract Database Types.

@inproceedings{DBLP:conf/pods/StempleS84,
  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        = {http://doi.acm.org/10.1145/588011.588047, db/conf/pods/StempleS84.html},
  crossref  = {DBLP:conf/pods/84},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Abstract

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.

• Windows: Click the letter of your CD drive
  A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
• UNIX/LINUX/Mac: use mount point /pods8298/... or /cdrom/...

• Windows: Click the letter of your CD drive
  A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
• UNIX/LINUX/Mac: use mount point /aDVD1/... or /cdrom/...

Printed Edition

Online Edition: ACM Digital Library

References

[BERN80]

Philip A. Bernstein, Barbara T. Blaustein, Edmund M. Clarke: Fast Maintenance of Semantic Integrity Assertions Using Redundant Aggregate Data. VLDB 1980: 126-136 BibTeX

[BERN81]

...

[BERN82]

Philip A. Bernstein, Barbara T. Blaustein: Fast Methods for Testing Quantified Relational Calculus Assertions. SIGMOD Conference 1982: 39-50 BibTeX

[BOYE79]

...

[BROD80]

Michael L. Brodie: The application of data types to database semantic integrity. Inf. Syst. 5(4): 287-296(1980) BibTeX

[BROD81]

Michael L. Brodie: Association: A Database Abstraction for Semantic Modelling. ER 1981: 577-602 BibTeX

[BUNE79]

Peter Buneman, Eric K. Clemons: Efficient Monitoring Relational Databases. ACM Trans. Database Syst. 4(3): 368-382(1979) BibTeX

[CLAY82]

Billy G. Claybrook: A Specification Method for Specifying Data and Procedural Abstractions. IEEE Trans. Software Eng. 8(5): 449-459(1982) BibTeX

[DATE83]

...

[EHRI78]

Hartmut Ehrig, Hans-Jörg Kreowski, Herbert Weber: Algebraic Specification Schemes for Data Base Systems. VLDB 1978: 427-440 BibTeX

[GARD79]

Georges Gardarin, Michel A. Melkanoff: Proving Consistency of Database Transactions. VLDB 1979: 291-298 BibTeX

[GERH83]

...

[HAMM78]

Michael Hammer, Sunil K. Sarin: Efficient Monitoring of Database Assertions (Abstract). SIGMOD Conference 1978: 159 BibTeX

[HOAR69]

C. A. R. Hoare: An Axiomatic Basis for Computer Programming. Commun. ACM 12(10): 576-580(1969) BibTeX

[LOCK78]

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

[MANN72]

Zohar Manna, Jean Vuillemin: Fix Point Approach to the Theory of Computation. Commun. ACM 15(7): 528-536(1972) BibTeX

[MCLE76]

...

[NICO83]

Jean-Marie Nicolas: Logic for Improving Integrity Checking in Relational Data Bases. Acta Inf. 18: 227-253(1982) BibTeX

[SANT80]

Clesio Saraiva dos Santos, Erich J. Neuhold, Antonio L. Furtado: A Data Type Approach to the Entity-Relationship Approach. ER 1979: 103-119 BibTeX

[SCHE80]

Peter Scheuermann, Gerd Schiffner, H. Weber: Abstraction Capabilities and Invariant Properties Modelling within the Entity-Relationship Approach. ER 1979: 121-140 BibTeX

[SCHM77]

Joachim W. Schmidt: Some High Level Language Constructs for Data of Type Relation. ACM Trans. Database Syst. 2(3): 247-261(1977) BibTeX

[SMIT80]

...

[TODD77]

...

[WALK81]

...

[VANE81]

...

[WEBE78]

Herbert Weber: A Software Engineering View of Data Base Systems. VLDB 1978: 36-51 BibTeX

[YEH77]

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