Abstract
We present an algorithm that takes a first-order sentence φ in full arithmetic with arrays (with quantification over numbers, and with numerical terms serving as array indices), and builds a test formula that can be used to determine which indices of φ's constituent arrays “really” occur. We call this concept syntactic dependence. We show how to use syntactic dependence as a test for semantic dependence, i.e., the true dependence of φ on the value of an array element. This is useful in truth-maintenance systems or symbolic execution systems, where a sentence may be true in one state but false in the next. More specifically, if we are given an initial state, a sentence (such as φ above) that is true in the initial state, and a list of array elements that may be changing value during a state transition, the algorithm can be used to determine whether φ must remain true after the state transition.
Get full access to this article
View all access options for this article.