Automatic generation of simplified weakest preconditions for integrity constraint verification

TL;DR

This paper introduces an automated method for generating simplified weakest preconditions to verify database integrity constraints after updates, applicable to relational and deductive databases, enhancing efficiency and correctness.

Contribution

It presents a novel confluent rewriting system for automatically deriving simplified weakest preconditions for database updates, extending to deductive databases with a formal proof.

Findings

Automated derivation of simplified weakest preconditions for relational databases.

Extension of the method to deductive databases with formal proof.

Ensures post-update constraints are maintained when preconditions are satisfied.

Abstract

Given a constraint $c$ assumed to hold on a database $B$ and an update $u$ to be performed on $B$, we address the following question: will $c$ still hold after $u$ is performed? When $B$ is a relational database, we define a confluent terminating rewriting system which, starting from $c$ and $u$, automatically derives a simplified weakest precondition $wp(c,u)$ such that, whenever $B$ satisfies $wp(c,u)$, then the updated database $u(B)$ will satisfy $c$, and moreover $wp(c,u)$ is simplified in the sense that its computation depends only upon the instances of $c$ that may be modified by the update. We then extend the definition of a simplified $wp(c,u)$ to the case of deductive databases; we prove it using fixpoint induction.