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 domain 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