Data constraints are fundamental for practical data modelling, and a verifiable conformance of a data instance to a safety-critical constraint (satisfaction relation) is a corner-stone of safety assurance. Diagrammatic constraints are important as both a theoretical concepts and a practically convenient device. The paper shows that basic formal constraint management can well be developed within a finitely complete category (hence the reference to Cartesianity in the title). In the data modelling context, objects of such a category can be thought of as graphs, while their morphisms play two roles: of data instances and (when being additionally labelled) of constraints. Specifically, a generalized sketch $S$ consists of a graph $G_S$ and a set of constraints $C_S$ declared over $G_S$, and appears as a pattern for typical data schemas (in databases, XML, and UML class diagrams). Interoperability of data modelling frameworks (and tools based on them) very much depends on the laws regulating the transformation of satisfaction relations between data instances and schemas when the schema graph changes: then constraints are translated co- whereas instances contra-variantly. Investigation of this transformation pattern is the main mathematical subject of the paper
翻译:摘要:数据约束是实践数据建模的基础,数据实例对安全关键约束的可验证符合性(满足关系)是安全保证的基石。图示约束既是理论概念,也是具有实际便利性的工具。本文表明,基本形式化约束管理可以在有限完备范畴中良好发展(因此标题中提及“笛卡尔性”)。在数据建模语境下,此类范畴的对象可视为图,而其态射则扮演双重角色:数据实例(以及附加标签时的)约束。具体而言,广义草图$S$由图$G_S$和声明于$G_S$上的约束集$C_S$构成,并作为典型数据模式(如数据库、XML和UML类图)的范型。数据建模框架(及其支撑工具)的互操作性高度依赖于如下规律:当模式图变化时,数据实例与模式间满足关系的变换必须满足协变约束翻译与逆变实例转换的调控规则。对该变换模式的研究是本文的主要数学主题。