Verifiable properties of database transactions

It is often necessary to ensure that database transactions preserve integri ty constraints that specify valid database states. While it is possible to monitor for violations of constraints at run-time, rolling back transaction s when violations are detected, it is preferable to verify correctness stat ically, before transactions are executed. This can be accomplished if we ca n verify transaction safety with respect to a set of constraints by means o f calculating weakest preconditions. We study properties of weakest precond itions for a number of transaction and specification languages. We show tha t some simple transactions do not admit weakest preconditions over first-or der logic and some of its extensions such as first-order logic with countin g and monadic Sigma(1)(1). We also show that the class of transactions that admit weakest preconditions over first-order logic cannot be captured by a ny transaction language. We consider a strong local form of verifiability, and show that it is different from the general form. We define robustly ver ifiable transactions as those that can be statically analyzed regardless of extensions to the signature of the specification language, and we show tha t the class of robustly verifiable transactions over first-order logic is e xactly the class of transactions that admit the local form of verifiability . We discuss the implications of these results for the design of verifiable transaction languages. (C) 1998 Academic Press.