Automatic generation of simplified weakest preconditions for integrity constraint verification

Details Automatic generation of simplified weakest preconditions for integrity constraint verification Automatic generation of simplified weakest preconditions for integrity constraint verification

2006-03-14

arxiv.org/abs/cs/0603053v1

Computer Science

Data Structures and Algorithms

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

Automatic generation of simplified weakest preconditions for integrity constraint verification does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Automatic generation of simplified weakest preconditions for integrity constraint verification, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Automatic generation of simplified weakest preconditions for integrity constraint verification will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-704661