Proving Consistency of Database Transactions.

@inproceedings{DBLP:conf/vldb/GardarinM79,
  author    = {Georges Gardarin and
               Michel A. Melkanoff},
  editor    = {Antonio L. Furtado and
               Howard L. Morgan},
  title     = {Proving Consistency of Database Transactions},
  booktitle = {Fifth International Conference on Very Large Data Bases, October
               3-5, 1979, Rio de Janeiro, Brazil, Proceedings},
  publisher = {IEEE Computer Society},
  year      = {1979},
  pages     = {291-298},
  ee        = {db/conf/vldb/GardarinM79.html},
  crossref  = {DBLP:conf/vldb/79},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Abstract

The purpose of this paper is to present an approach for verifying that explicitely stated integrity constraints are not violated by certain transactions. We utilize a relational model wherein constraints are given in a language based on the first order predicate calculus. Transactions are written in terms of an ALGOL60 like host language with embedded first order predicate calculus capabilities allowing queries and updates.

The technique for proving consistency of the transactions is based upon the Hoare axiomatic approach: We illustrate the method by means of an explicit example of a database updated by four types of transaction. A generalized transaction consistency verifier embodying this approach would considerably enhance transaction programming in a relational database management system.

Copyright © 1979 by The Institute of Electrical and Electronic Engineers, Inc. (IEEE). Abstract used with permission.

ACM SIGMOD Anthology

• 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
• Mac: Click here
• UNIX/LINUX: mount the CD and click on the path of your mount point:
  /Anthology/vldb7588 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
• Mac: Click here
• UNIX/LINUX: mount the DVD and click on the path of your mount point:
  /Anthology/aDVD1 or /dvd

Printed Edition

References

[1]

...

[2]

...

[3]

E. F. Codd: A Relational Model of Data for Large Shared Data Banks. Commun. ACM 13(6): 377-387(1970) BibTeX

[4]

Kapali P. Eswaran, Jim Gray, Raymond A. Lorie, Irving L. Traiger: The Notions of Consistency and Predicate Locks in a Database System. Commun. ACM 19(11): 624-633(1976) BibTeX

[5]

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

[6]

John H. Howard: Proving Monitors. Commun. ACM 19(5): 273-279(1976) BibTeX

[7]

...

[8]

Susan S. Owicki, David Gries: Verifying Properties of Parallel Programs: An Axiomatic Approach. Commun. ACM 19(5): 279-285(1976) BibTeX

[9]

...

[10]

...

[11]

Michael Stonebraker, Eugene Wong, Peter Kreps, Gerald Held: The Design and Implementation of INGRES. ACM Trans. Database Syst. 1(3): 189-222(1976) BibTeX

[12]

Michael Stonebraker, Lawrence A. Rowe: Observations on Data Manipulation Languages and Their Embedding in General Purpose Programming Languages. VLDB 1977: 128-143 BibTeX

[13]

...

Referenced by

1. Véronique Benzaken, Xavier Schaefer: Static Management of Integrity in Object-Oriented Databases: Design and Implementation. EDBT 1998: 311-325
2. Dimitris Plexousakis, John Mylopoulos: Accomodating Integrity Constraints During Database Design. EDBT 1996: 497-513
3. Véronique Benzaken, Anne Doucet: Thémis: A Database Programming Language Handling Integrity Constraints. VLDB J. 4(3): 493-517(1995)
4. Xiaolei Qian: The Deductive Synthesis of Database Transactions. ACM Trans. Database Syst. 18(4): 626-677(1993)
5. Véronique Benzaken, Anne Doucet: Thémis: a database programming language with integrity constraints. DBPL 1993: 243-262
6. H. V. Jagadish, Xiaolei Qian: Integrity Maintenance in Object-Oriented Databases. VLDB 1992: 469-480
7. Tim Sheard, David W. Stemple: Automatic Verification of Database Transaction Safety. ACM Trans. Database Syst. 14(3): 322-368(1989)
8. Xiaolei Qian, Richard J. Waldinger: A Transaction Logic for Database Specification. SIGMOD Conference 1988: 243-250
9. Subhasish Mazumdar, David W. Stemple, Tim Sheard: Resolving the Tension between Integrity and Security Using a Theorem Prover. SIGMOD Conference 1988: 233-242
10. Udo W. Lipeck: Transformation of Dynamic Integrity Constraints into Transaction Specifications. ICDT 1988: 322-337
11. Udo W. Lipeck: Stepwise Specification of Dynamic Database Behaviour. SIGMOD Conference 1986: 387-397
12. Tim Sheard, David W. Stemple: Coping with Complexity in Automated Reasoning about Database Systems. VLDB 1985: 426-435
13. Serge Abiteboul, Victor Vianu: Transactions and Integrity Constraints. PODS 1985: 193-204
14. Hervé Gallaire, Jack Minker, Jean-Marie Nicolas: Logic and Databases: A Deductive Approach. ACM Comput. Surv. 16(2): 153-185(1984)
15. Eric Simon, Patrick Valduriez: Design and Implementation of an Extendible Integrity Subsystem. SIGMOD Conference 1984: 9-17
16. David W. Stemple, Tim Sheard: Specification and Verification of Abstract Database Types. PODS 1984: 248-257
17. Armin B. Cremers, G. Doman: AIM - An Integrity Monitor for the Database System INGRES. VLDB 1983: 167-170
18. Dipayan Gangopadhyay, Umeshwar Dayal, James C. Browne: Semantics of Network Data Manipulation Languages: An Object-Oriented Approach. VLDB 1982: 357-369
19. Philip A. Bernstein, Barbara T. Blaustein: Fast Methods for Testing Quantified Relational Calculus Assertions. SIGMOD Conference 1982: 39-50
20. Hervé Gallaire: Impacts of Logic and Databases (Invited Paper). VLDB 1981: 248-259
21. Alexander Borgida, Harry K. T. Wong: Data Models and Data Manipulation Languages: Complementary Semantics and Proof Theory. VLDB 1981: 260-271
22. Jean Le Bihan, Christian Esculier, Gérard Le Lann, Witold Litwin, Georges Gardarin, S. Sedillort, L. Treille: SIRIUS: A French Nationwide Project on Distributed Data Bases. VLDB 1980: 75-85