Quantifiers

 

QuantifierExpression ::= 
    QuantifierKeyword "[" Ident "]" 
      "IN" Expression ":-" Expression |
    QuantifierKeyword "IN" Expression 
      ":-" Expression

QuantifierKeyword ::= "FOR_ALL" | "THERE_IS" | "COUNT" | 
		      "FIRST" | "LAST"

A quantifier expression takes a list, bounds a free variable to each value of this list in sequence, and evaluates a user-defined expression for each of these values. This user-defined expression must evaluate to a boolean.

Then, depending on the very nature of the quantifier, that is, the first keyword which has been used, different kinds of information will be returned:

FOR_ALL

the quantifier returns TRUE if no element from the original list caused the filter expression to evaluate to FALSE.

THERE_IS

the quantifier returns TRUE if at least one element from the original list caused the filter expression to evaluate to TRUE.

COUNT

the quantifier returns the number of elements from the original list that caused the filter expression to evaluate to TRUE.

FIRST

the quantifier returns the first element from the original list that caused the filter expression to evaluate to TRUE.

LAST

the quantifier returns the last element from the original list that caused the filter expression to evaluate to TRUE.

For instance, given:

a := {1, 3, 6, 10, 20, 40, 1000}

we have:

ASSERT THERE_IS IN a :- X+1 MOD 7 = 0;  -- 20
ASSERT FOR_ALL IN a :- X MOD 7 <> 0; 
ASSERT 2 = COUNT IN a :- X MOD 2 <> 0; 
ASSERT 5 = COUNT IN a :- X MOD 2 = 0; 
ASSERT 20 = FIRST IN a :- X MOD 20 = 0; 
ASSERT 1000 = LAST IN a :- X MOD 20 = 0;