Formal Specification By Coq Of Date And Darwen’s Object/relational Model

Development of databases software systems would be provided with a high-level specification, suitable for formal reasoning about application-level security and correctness properties. Formal specification is a key element of formal methods. It can greatly increase comprehension of a system by revealing inconsistencies, ambiguities, and incompleteness that might occur. Thus, implementation would be proven correct with respect to this specification to ensure that a bug cannot lead to non-conformance of properties or accidental corruption. It is for these reasons that we see verified DBMSs as a compelling challenge to the development of software. As a step toward this goal, we establish in this paper formalization through a formal specification of some basis concepts in object/relational model proposed by Date and Darwen, using the Coq proof assistant system. We give the challenges acquired from our experience using that proof tool. Our work is a preamble step toward a fully-verified object/relational DBMS.