Proving Consistency Of Database Transactions

The purpose of this paper is to present an approach for verifying that explicitely stated integrity constraints are not violated by certain transactions. We utilize a relational model where-in constraints are given in a language based on the first order predicate calculus. Transactions are written in terms of an ALGOL.60 like host language with embedded first order predicate calculus capabilities allowing queries and updates. The technique for proving consistency of the transactions is based upon the Hoare axiomatic approach. We illustrate the method by means of an explicit example of a database updated by four types of transaction. A generalized transaction consistency verifier embodying this approach would considerably enhance transaction programming in a relational database management system.