Design of an Automatic Prover Dedicated to the Refinement of Database Applications

The paper presents an approach that enables the elaboration of an automatic prover dedicated to the refinement of database applications. The approach is based on a strategy of proof reuse and on the specific characteristics of such applications. The problem can be stated as follows. Having established a set of basic refinement proofs associated to a set of refinement rules, the issue is to study how these basic proofs can be reused to establish more elaborate refinements. Elaborate refinements denote refinements that require the application of more than one refinement rule. We consider the B refinement process. In B, substitutions are inductively built using constructors. For each B constructor, we have formally defined the necessary and sufficient conditions that enable the reuse of the basic proofs. An application of our approach to data-intensive applications is presented