10.34.9.6 Execution of Propagating Indexicals

Consider the definition of a constraint C containing a propagating indexical X in R. Let \TV(X,C,S) denote the set of values for X that can make C true in some ground extension of the store S. Then the indexical should obey the following coding rules:

If the coding rules are observed, S(R) can be proven to contain \TV(X,C,S) for all stores in which R is monotone. Hence it is natural for the implementation to wait until R becomes monotone before admitting the propagating indexical for execution. The execution of X in R thus involves the following:

A propagating indexical is scheduled for execution as follows:


Send feedback on this subject.