Verify updating trigger correctness

Abstract

One of the major applications of trigger rules is to maintain database integrity. However, since trigger rules, like computer programs, may not be written correctly, it is important to have tools to verify the correctness. Generally, this is an undecidable problem. Only few works exist on this problem. However, most of these works either depend on human inspection, or incur a run-time overhead. In this paper, we introduce a new approach which does not depend on any human judgment nor any run-time monitoring. The trigger rules we are checking are those trigger rules which update object properties but do not insert any new object nor destroy an existing object. The constraints in our paper do not have any existential quantifier. If our method returns "yes", we can guarantee that the set of trigger rules are written correctly to enforce the given constraint.