|
|
|
@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}
}
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.
