Proving Consistency of Database Transactions.

Georges Gardarin, Michel A. Melkanoff: Proving Consistency of Database Transactions. VLDB 1979: 291-298
  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,}


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

CDROM Version: Load the CDROM "Volume 1 Issue 4, VLDB '75-'88" and ... DVD Version: Load ACM SIGMOD Anthology DVD 1" and ... BibTeX

Printed Edition

Antonio L. Furtado, Howard L. Morgan (Eds.): Fifth International Conference on Very Large Data Bases, October 3-5, 1979, Rio de Janeiro, Brazil, Proceedings. IEEE Computer Society 1979
Contents BibTeX


E. F. Codd: A Relational Model of Data for Large Shared Data Banks. Commun. ACM 13(6): 377-387(1970) BibTeX
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
C. A. R. Hoare: An Axiomatic Basis for Computer Programming. Commun. ACM 12(10): 576-580(1969) BibTeX
John H. Howard: Proving Monitors. Commun. ACM 19(5): 273-279(1976) BibTeX
Susan S. Owicki, David Gries: Verifying Properties of Parallel Programs: An Axiomatic Approach. Commun. ACM 19(5): 279-285(1976) BibTeX
Michael Stonebraker, Eugene Wong, Peter Kreps, Gerald Held: The Design and Implementation of INGRES. ACM Trans. Database Syst. 1(3): 189-222(1976) BibTeX
Michael Stonebraker, Lawrence A. Rowe: Observations on Data Manipulation Languages and Their Embedding in General Purpose Programming Languages. VLDB 1977: 128-143 BibTeX

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
ACM SIGMOD Anthology - DBLP: [Home | Search: Author, Title | Conferences | Journals]
VLDB Proceedings (1977-1981): Copyright © by IEEE,
ACM SIGMOD Anthology: Copyright © by ACM (, Corrections:
DBLP: Copyright © by Michael Ley (, last change: Sat May 16 23:45:06 2009