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)

[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)

[5]

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

[6]

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

[7]

...

[8]

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

[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)

[12]

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

[13]

...