A transaction logic for database specification
Xiaolei Qian, Richard J. Waldinger · ACM SIGMOD Record · 1988
We introduce a logical formalism for the specification of the dynamic behavior of databases. The evolution of databases is characterized by both the dynamic integrity constraints which describe the properties of state transitions and the transactions whose executions lead to state transitions. Our formalism is based on a variant of first-order situational logic in which the states of computations are explicit objects. Integrity constraints and transactions are uniformly specifiable as expressions in our language. We also point out the application of the formalism to the verification and synthesis of transactions.