In the context of the model-driven development of data-centric applications, OCL constraints play a major role in adding precision to the source models (e.g., data models and security models). Several code-generators have been proposed to bridge the gap between source models with OCL constraints and their corresponding database implementations. However, the database queries produced by these code-generators are significantly less efficient -- from the point of view of execution-time performance -- than the implementations manually written by database experts. In this paper, we propose a different approach to bridge the gap between models with OCL constraints and their corresponding database implementations. In particular, we introduce a model-based methodology for proving the correctness of manually written SQL implementations of OCL constraints. This methodology is based on a novel mapping from a significant subset of the SQL language into many-sorted first-order logic. Moreover, by leveraging on an already existing mapping from the OCL language into many-sorted first-order logic, we can use SMT solvers to automatically prove the correctness of SQL implementations of OCL constraints. To illustrate and show the applicability of our approach, we include in the paper a number of non-trivial examples. Finally, we report on the status of a suite of tools supporting our approach.

翻译：在以数据为中心的应用程序模型驱动开发背景下，OCL约束在提升源模型（如数据模型与安全模型）的精确性方面发挥着重要作用。已有多种代码生成器被提出以弥合含OCL约束的源模型与其对应数据库实现之间的鸿沟。然而，从执行时间性能角度来看，这些代码生成器产生的数据库查询效率显著低于数据库专家手工编写的实现。本文提出一种弥合含OCL约束的模型与其数据库实现之间鸿沟的新方法。具体而言，我们引入一种基于模型的方法论，用于证明手工编写的OCL约束SQL实现的正确性。该方法论基于从SQL语言重要子集到多类一阶逻辑的新型映射。此外，通过利用已存在的从OCL语言到多类一阶逻辑的映射，我们可使用SMT求解器自动证明OCL约束SQL实现的正确性。为说明并展示本方法的适用性，文中包含若干非平凡示例。最后，我们报告了支持本方法的一套工具集的现状。