All-quantified predicates

Normally all predicates are existentially quantified in their variables. However, one predicate in a rule is allowed to be preceeded by an all quantifier, e.g. FORALL V: p(X, V). The all-quantified variable must be the right variable of the predicate. Predicates in the head of a rule cannot be all-quantified. Currently the concept of all-quantifiers is rather restricted. It works only in two situations:

• The all-quantified variable is the middle variable of a path with two predicates and the rule test is a single path. This is the standard situation for MUST dataflow analyses (section 5.2.2).
• The all-quantified variable is the sink of an rule test graph. This rule test graph must also be either a path or a dag (see example specification copyprop.ox).