Proving Consistency Of Database Transactions
- 25 August 2005
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 291-298
- https://doi.org/10.1109/vldb.1979.718144
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.Keywords
This publication has 5 references indexed in Scilit:
- The notions of consistency and predicate locks in a database systemCommunications of the ACM, 1976
- Verifying properties of parallel programsCommunications of the ACM, 1976
- Proving monitorsCommunications of the ACM, 1976
- A relational model of data for large shared data banksCommunications of the ACM, 1970
- An axiomatic basis for computer programmingCommunications of the ACM, 1969