Proving Consistency Of Database Transactions

TLDR

The paper proposes a method to verify that explicitly stated integrity constraints are not violated by specific transactions. The authors use a relational model with first‑order predicate‑calculus constraints, encode transactions in an ALGOL.60‑like language, and apply a Hoare‑axiomatic approach to prove consistency, illustrated with a four‑transaction example. The proposed verifier would significantly improve transaction programming in relational database systems.

Abstract

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.