Automatic generation of simplified weakest preconditions for integrity constraint verification
| dc.creator | -Bouziad, A. Ai T | |
| dc.creator | Guessarian, Irene | |
| dc.creator | Vieille, L. | |
| dc.date | 2006-03-14 | |
| dc.date.accessioned | 2026-07-07T07:05:50Z | |
| dc.date.available | 2026-07-07T07:05:50Z | |
| dc.description | 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. | |
| dc.identifier | https://arxiv.org/abs/cs/0603053 | |
| dc.identifier | http://arxiv.org/abs/cs/0603053 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/109808 | |
| dc.subject | Data Structures and Algorithms | |
| dc.subject | Databases | |
| dc.title | Automatic generation of simplified weakest preconditions for integrity constraint verification | |
| dc.type | text |