Indexicals

An indexical is a reactive functional rule of the form X in R, where R is a set valued range expression (see below). See Syntax of Indexicals, for a grammar defining indexicals and range expressions.

Indexicals can play one of two roles: propagating indexicals are used for constraint solving, and checking indexicals are used for entailment checking. When a propagating indexical fires, R is evaluated in the current store S, which is extended by adding the new domain constraint X::S(R) to the store, where S(R) denotes the value of R in S. When a checking indexical fires, it checks if D(X,S) is contained in S(R), and if so, the constraint corresponding to the indexical is detected as entailed.