ACM SIGMOD Anthology VLDB dblp.uni-trier.de

Proving Consistency of Database Transactions.

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

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

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 CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML

References

[1]
...
[2]
...
[3]
E. F. Codd: A Relational Model of Data for Large Shared Data Banks. Commun. ACM 13(6): 377-387(1970) CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[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) CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[5]
C. A. R. Hoare: An Axiomatic Basis for Computer Programming. Commun. ACM 12(10): 576-580(1969) CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[6]
John H. Howard: Proving Monitors. Commun. ACM 19(5): 273-279(1976) CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[7]
...
[8]
Susan S. Owicki, David Gries: Verifying Properties of Parallel Programs: An Axiomatic Approach. Commun. ACM 19(5): 279-285(1976) CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[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) CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[12]
Michael Stonebraker, Lawrence A. Rowe: Observations on Data Manipulation Languages and Their Embedding in General Purpose Programming Languages. VLDB 1977: 128-143 CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[13]
...

Copyright © Mon Mar 15 03:55:47 2010 by Michael Ley (ley@uni-trier.de)