Designing consistency-preserving database transactions

Transaction programs by definition have to maintain all consistency constraints defined on a database. Although the overall operational consistency of a database rests on this crucial assumption, there are few design aids to support the design of consistent transaction programs. An approach is presented for verifying that the defined integrity constraints are not violated by a transaction program. Assuming that the database is in a consistent state before the transaction program starts, the database stays consistent after the execution of a correct transaction program. In this approach all computations and all modifications on the database are identified and represented with symbolic values. The symbolic representation of the output variables and database operations is used to verify the integrity constraints. Therefore, it is possible to support the application programmer in designing correct transaction programs