Synthesizing Database Transactions
Xiaolei Qian · 1990
Database programming requires having the knowledge of database semantics both to maintain database integrity and to explore more optimization opportunities. Automated pro-gramming of database transactions is desirable and feasible. In general, transactions use simple constructs and algorithms; specifications of database semantics are available; and trans-actions perform small incremental updates to database con-tents. 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 tachniques. A transaction logic is developed as the formalism with which the synthesis is conducted. Transactions are gen-erated 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. 1