Synthesizing Database Transactions.

@inproceedings{DBLP:conf/vldb/Qian90,
  author    = {Xiaolei Qian},
  editor    = {Dennis McLeod and
               Ron Sacks-Davis and
               Hans-J{\"o}rg Schek},
  title     = {Synthesizing Database Transactions},
  booktitle = {16th International Conference on Very Large Data Bases, August
               13-16, 1990, Brisbane, Queensland, Australia, Proceedings},
  publisher = {Morgan Kaufmann},
  year      = {1990},
  isbn      = {1-55860-149-X},
  pages     = {552-565},
  ee        = {db/conf/vldb/Qian90.html},
  crossref  = {DBLP:conf/vldb/90},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Abstract

Database programming requires having the knowledge of database semantics both to maintain database integrity and to explore more optimization opportunities. Automated programming of database transactions is desirable and feasible. In general, transactions use simple constructs and algorithms; specifications of database semantics are available; and transactions perform small incremental updates to database contents. Automated programming in such a restricted but well- understood and important domain is promising.

We approach the synthesis of database transactions that preserve the validity of integrity constraints using deductive techniques. A transaction logic is developed as the formalism with which the synthesis is conducted. Transactions are generated as the by-product of proving specifications in the logic. The Manna-Waldinger deductive-tableau system is extended with inference rules for the extraction of transactions from proofs, which require the cooperation of multiple tableaux.

Copyright © 1990 by the VLDB Endowment. Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the VLDB copyright notice and the title of the publication and its date appear, and notice is given that copying is by the permission of the Very Large Data Base Endowment. To copy otherwise, or to republish, requires a fee and/or special permission from the Endowment.

Online Paper

• Download PDF file (www.vldb.org, Darmstadt, Germany)
• Download PDF file (www.acm.org, New York, USA)

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/vldb8997 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

Journal Version

References

[1]

...

[2]

Marco A. Casanova, Philip A. Bernstein: A Formal System for Reasoning about Programs Accessing a Relational Database. ACM Trans. Program. Lang. Syst. 2(3): 386-414(1980) BibTeX

[3]

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

[4]

Johann Christoph Freytag, Nathan Goodman: On the Translation of Relational Queries into Iterative Programs. ACM Trans. Database Syst. 14(1): 1-27(1989) BibTeX

[5]

...

[6]

...

[7]

...

[8]

Zohar Manna, Richard J. Waldinger: A Deductive Approach to Program Synthesis. ACM Trans. Program. Lang. Syst. 2(1): 90-121(1980) BibTeX

[9]

Zohar Manna, Richard J. Waldinger: Problematic Features of Programming Languages: A Situational-Calculus Approach. Acta Inf. 16: 371-426(1981) BibTeX

[10]

Zohar Manna, Richard J. Waldinger: The Deductive Synthesis of Imperative LISP Programs. AAAI 1987: 155-160 BibTeX

[11]

Zohar Manna, Richard J. Waldinger: How to Clear a Block: A Theory of Plans. J. Autom. Reasoning 3(4): 343-377(1987) BibTeX

[12]

...

[13]

...

[14]

Jean-Marie Nicolas, Hervé Gallaire: Data Base: Theory vs. Interpretation. Logic and Data Bases 1977: 33-54 BibTeX

[15]

...

[16]

...

[17]

...

[18]

Tim Sheard, David W. Stemple: Automatic Verification of Database Transaction Safety. ACM Trans. Database Syst. 14(3): 322-368(1989) BibTeX

[19]

Jeffrey D. Ullman: Principles of Database and Knowledge-Base Systems, Volume I. Computer Science Press 1988, ISBN 0-7167-8158-1
Contents BibTeX

[20]

...