Incorporating theory into database system development

摘要

Database systems, like all models, must be constrained to represent just those states and transitions which are possible in the world they model. Database integrity constraints, transition constraints and transaction definitions specify the conformity of a database system to the real world. The enforcement of database system constraints is a difficult problem to solve efficiently; this follows from the large amounts of data involved and the complexity of determining minimum required checks. We present a database system development method in which considerable theoretical support in the form of automated theorem proving is brought to bear on the integrity enforcement problem.