Automatic generation of simplified weakest preconditions for integrity constraint verification
<|reference_start|>Automatic generation of simplified weakest preconditions for integrity constraint verification: 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.<|reference_end|>
@article{-bouziad2006automatic,
    title={Automatic generation of simplified weakest preconditions for integrity
  constraint verification},
    author={A. Ai T -Bouziad (LIAFA), Irene Guessarian (LIAFA), L. Vieille (NCM)},
    journal={arXiv preprint arXiv:cs/0603053},
    year={2006},
    archivePrefix={arXiv},
    eprint={cs/0603053},
    primaryClass={cs.DS cs.DB}
}