Next: Compiled Indexicals, Previous: Execution of Propagating Indexicals, Up: Defining Primitive Constraints [Contents][Index]
Consider the definition of a constraint C containing a checking
indexical X in R
. Let FV(X,C,S) denote the set
of values for X that can make C false in some ground
extension of the store S. Then the indexical should obey the
following coding rules:
If the coding rules are observed, then S(R) can be proven to exclude
FV(X,C,S) for all stores in which R is anti-monotone. Hence
it is natural for the implementation to wait until R becomes
anti-monotone before admitting the checking indexical for execution.
The execution of X in R
thus involves the following:
A checking indexical is scheduled for execution as follows:
dom(Y)
or card(Y)
in R has been pruned
min(Y)
in R has been increased
max(Y)
in R has been decreased