10.10.10.9 Execution of Checking Indexicals
Consider the definition of a constraint C containing a checking
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:
- all arguments of C except X should occur in R
- if R is ground in S, S(R) = TV(X,C,S)
If the coding rules are observed, 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:
- If D(X,S) is contained in S(R), none of the possible values
for X can make C false, and so C is detected as
- Otherwise, if D(X,S) is disjoint from S(R) and R is
ground in S, all possible values for X will make C
false, and so C is detected as disentailed.
- Otherwise, D(X,S) contains some values that could make C
true and some that could make C false, and the indexical suspends.
A checking indexical is scheduled for execution as follows:
- it is evaluated initially as soon as it has become anti-monotone
- it is re-evaluated when one of the following conditions occurs:
- the domain of X has been pruned, or X has been assigned
- the domain of a variable Y that occurs as
) in R has been pruned
- the lower bound of a variable Y that occurs as
in R has been increased
- the upper bound of a variable Y that occurs as
in R has been decreased
Send feedback on this subject.