Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Simplified integrity checking for an expressive class of denial constraints

Davide Martinenghi

TL;DR

The paper tackles efficient integrity-checking for expressive denial constraints by introducing a transformation-based framework that converts complex constraints into simplified pre-tests. It defines two non-recursive languages, ${\cal L}_{\sf S}$ and ${\cal L}_{\sf H}$, and a two-step procedure (After and Optimize) to compute weakest preconditions and conditional weakest preconditions that preserve semantical equivalence under updates. Central contributions include formalizing WP/CWP, unfolding mechanisms to remove intensional predicates, and handling negated existential quantifiers through extended denials, all while ensuring termination and tractability. The approach supports direct SQL translation and integration with active databases, offering a practical path to design-time, automated integrity checking with potential for broader extensions and cost-aware optimization.

Abstract

Data integrity is crucial for ensuring data correctness and quality, maintained through integrity constraints that must be continuously checked, especially in data-intensive systems like OLTP. While DBMSs handle common constraints well, complex constraints often require ad-hoc solutions. Research since the 1980s has focused on automatic and simplified integrity constraint checking, leveraging the assumption that databases are consistent before updates. This paper discusses using program transformation operators to generate simplified integrity constraints, focusing on complex constraints expressed in denial form. In particular, we target a class of integrity constraints, called extended denials, which are more general than tuple-generating dependencies and equality-generating dependencies. These techniques can be readily applied to standard database practices and can be directly translated into SQL.

Simplified integrity checking for an expressive class of denial constraints

TL;DR

The paper tackles efficient integrity-checking for expressive denial constraints by introducing a transformation-based framework that converts complex constraints into simplified pre-tests. It defines two non-recursive languages, and , and a two-step procedure (After and Optimize) to compute weakest preconditions and conditional weakest preconditions that preserve semantical equivalence under updates. Central contributions include formalizing WP/CWP, unfolding mechanisms to remove intensional predicates, and handling negated existential quantifiers through extended denials, all while ensuring termination and tractability. The approach supports direct SQL translation and integration with active databases, offering a practical path to design-time, automated integrity checking with potential for broader extensions and cost-aware optimization.

Abstract

Data integrity is crucial for ensuring data correctness and quality, maintained through integrity constraints that must be continuously checked, especially in data-intensive systems like OLTP. While DBMSs handle common constraints well, complex constraints often require ad-hoc solutions. Research since the 1980s has focused on automatic and simplified integrity constraint checking, leveraging the assumption that databases are consistent before updates. This paper discusses using program transformation operators to generate simplified integrity constraints, focusing on complex constraints expressed in denial form. In particular, we target a class of integrity constraints, called extended denials, which are more general than tuple-generating dependencies and equality-generating dependencies. These techniques can be readily applied to standard database practices and can be directly translated into SQL.
Paper Structure (9 sections, 4 theorems, 30 equations, 1 figure)

This paper contains 9 sections, 4 theorems, 30 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Relational and deductive databases
  3. A simplification procedure for obtaining a pre-test
  4. Generating weakest preconditions
  5. Simplification in ${\cal L}_{\hbox{\tiny{\sf S}}}$
  6. Denials with negated existential quantifiers
  7. Examples
  8. Related work
  9. Conclusion

Key Result

Proposition 4.5

Let $S\in{\cal L}_{\hbox{\tiny{{\sf H}}}}$. Then $\hbox{\sf Unfold}_{{\cal L}_{\hbox{\tiny{{\sf H}}}}}(S)\equiv S$.

Figures (1)

  • Figure 1: The starred dependency graphs for the schemata of Example \ref{['ex:dependency-graph-starred']}.

Theorems & Definitions (41)

  • Definition 2.1: Schema, database
  • Definition 2.2: Update
  • Example 2.3
  • Definition 3.1: Weakest precondition
  • Definition 3.2: Conditional weakest precondition
  • Example 3.3
  • Definition 3.4: Starred dependency graph
  • Example 3.5
  • Definition 3.6: ${\cal L}_{\hbox{\tiny{\sf S}}}$
  • Example 3.7
  • ...and 31 more