Translating E/R-diagrams into consistent database specifications

Semi formal methods, for example those which are used
in the database community, are useful for communication between
developers and clients. But they are not useful for formal
verification.To overcome this problem it is possible to translate

E/R-diagrams into first order algebraic specifications. The aim of

our task was to prove the consistency of such translate
specifications. To realize the proof we use the KIV (Karlsruhe
Interactive Verifier) approach for the development of correct

large software systems, i.e. we prove the consistency indirect by

proving the correctness of an implementation. For this purpose we
automatically translate E/R-diagrams not only in an algebraic
specification, but in a modular system containing structured
specifications and implementations. For a concrete E/R-diagram we
can prove the correctness with the KIV system. Because the
translation is uniform a generalized handmade proof for arbitrary
but fixed E/R-diagrams is possible, and presented in this paper.

This paper also includes an exemplary translation of an
E/R-diagram with 5 entities and 6 relations. The generated modular
system contains 33 specifications with more than 300 specified
... mehroperations and more than 500 axioms. Furthermore the
implementation contains more than 2200 lines of code.