A systematic approach to generate B preconditions: Application to the database domain

Maintaining integrity constraints in information systems is a real issue. In our previous work, we have defined a formal approach that derives B formal specifications from a UML description of the system. Basically, the generated B specification is composed of a set of variables modeling data and a set of operations representing transactions. The integrity constraints are directly specified as B invariant properties. So far, the operations we generate establish only a reduced class of constraints. In this paper, we describe a systematic approach to identify preconditions that take a larger class of invariants into account. The key idea is the definition of rewriting and simplification rules that we apply to the B invariants.