The Deductive Synthesis of Database Transactions.

@article{DBLP:journals/tods/Qian93,
  author    = {Xiaolei Qian},
  title     = {The Deductive Synthesis of Database Transactions},
  journal   = {ACM Trans. Database Syst.},
  volume    = {18},
  number    = {4},
  year      = {1993},
  pages     = {626-677},
  ee        = {http://doi.acm.org/10.1145/169725.169716, db/journals/tods/Qian93.html},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Abstract

Database programming requires 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 domam is promising.

We approach the synthesis of database transactions that preserve the validity of integrity constraints using deductive techniques. A transaction logic for a fairly expressive class of transactions is developed as the formalism within 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 reference rules for tbe extraction of transactions from proofs, which require the cooperation of multiple tableaux. Control strategies are developed that utilize the database semantics to reduce search effort in the symthesis process and to enhance runtime efficiency of the generated transactions.

Copyright © 1993 by the ACM, Inc., used by permission. Permission to make digital or hard copies is granted provided that copies are not made or distributed for profit or direct commercial advantage, and that copies show this notice on the first page or initial screen of a display along with the full citation.

Joint ACM SIGMOD / IEEE Computer Society 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/An3-2 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/aDVD2 or /dvd

Online Edition: ACM Digital Library

Conference 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]

...

[5]

Ronald Fagin: Horn clauses and database dependencies. J. ACM 29(4): 952-985(1982) BibTeX

[6]

...

[7]

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

[8]

Georges Gardarin, Michel A. Melkanoff: Proving Consistency of Database Transactions. VLDB 1979: 291-298 BibTeX

[9]

...

[10]

Jean-Yves Girard: A New Constructive Logic: Classical Logic. Mathematical Structures in Computer Science 1(3): 255-296(1991) BibTeX

[11]

...

[12]

Lawrence J. Henschen, William McCune, Shamim A. Naqvi: Compiling Constraint-Checking Programs from First-Order Formulas. Advances in Data Base Theory 1982: 145-169 BibTeX

[13]

Arding Hsu, Tomasz Imielinski: Integrity Checking for Multiple Updates. SIGMOD Conference 1985: 152-168 BibTeX

[14]

Elaine Kant: On the Efficient Synthesis of Efficient Programs. Artif. Intell. 20(3): 253-305(1983) BibTeX

[15]

...

[16]

Shaye Koenig, Robert Paige: A Transformational Framework for the Automatic Control of Derived Data. VLDB 1981: 306-318 BibTeX

[17]

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

[18]

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

[19]

Zohar Manna, Richard J. Waldinger: Special relations in automated deduction. J. ACM 33(1): 1-59(1986) BibTeX

[20]

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

[21]

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

[22]

...

[23]

Alberto Martelli, Corrado Moiso, Gianfranco Rossi: An Algorithm for Unification in Equational Theories. SLP 1986: 180-186 BibTeX

[24]

...

[25]

...

[26]

...

[27]

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

[28]

Jean-Marie Nicolas: Logic for Improving Integrity Checking in Relational Data Bases. Acta Inf. 18: 227-253(1982) BibTeX

[29]

Robert Paige: Applications of Finite Differencing to Database Integrity Control and Query/Transaction Optimization. Advances in Data Base Theory 1982: 171-209 BibTeX

[30]

...

[31]

...

[32]

Xiaolei Qian: An Axiom System for Database Transactions. Inf. Process. Lett. 36(4): 183-189(1990) BibTeX

[33]

Xiaolei Qian: The Expressive Power of the Bounded-Iteration Construct. Acta Inf. 28(7): 631-656(1991) BibTeX

[34]

...

[35]

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

[36]

Douglas R. Smith: Top-Down Synthesis of Divide-and-Conquer Algorithms. Artif. Intell. 27(1): 43-96(1985) BibTeX

[37]

Mark E. Stickel: Automated Deduction by Theory Resolution. J. Autom. Reasoning 1(4): 333-355(1985) BibTeX

[38]

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

[39]

...

[40]

...

Referenced by

1. Véronique Benzaken, Xavier Schaefer: Static Management of Integrity in Object-Oriented Databases: Design and Implementation. EDBT 1998: 311-325