Specification-based Approach for Denotational Semantic of Orthogonal Object/Relational DBMS

The issue of the article is at the crossroads of databases modeling, software engineering and databases verification using formal methods. Development of databases software would be provided with a high-level specification suitable for formal reasoning about correctness properties. Formal specification techniques help discover problems in system requirements, inconsistencies and incompleteness can be resolved. Thus, we see a specified object/relational database management system (ORDBMS) as a compelling challenge. Toward this goal, we propose a formal specification–based approach to describe a denotational semantic of an orthogonal object/relational model, a compiler for SQL3 queries language and an implementation of execution engine of queries over imperative generic finite maps interface. This approach is of functional style based on inductive definitions and a high-order type theory realized within Coq proof assistant. Our work is a preamble step toward a verified ORDBMS.