Universal Class Instance Quantification

  Universal quantification is achieved as follows, for a quantified formula forall[var:QuantifiedClass].P(var)

1. For the bound variable var in the quantification, introduce a static field var of type QuantifiedClass in the public class BoundVariables. This will introduce a global state variable for each such field in the finite-state model for the program.
2. For each field in BoundVariables define a predicate var_selected which is true when var is not null.
3. At the end of each constructor for QuantifiedClass introduce the following code fragment:

   if (BoundVariables.var == null)
     if (Bandera.choose(true,false)) BoundVariables.var = this;

   where Bandera.choose(true,false) introduces a non-deterministic choice between true and false values in the finite-state model for the program.
4. The temporal formula, P, to be checked on the generated model is modified in two ways. First, the pattern, P, in the scope of the quantifier, is expanded using the name var as parameters to the referenced predicates; call this expanded formula P_var. Second, this expanded formula is embedded in a context which controls the sequences of states on which P_var is evaluated. Specifically, for LTL, the expanded formula has the form:

   (!var_selected U (var_selected && P_var)) || []!var_selected

Checking the modified formula on the modified model exploits the exhaustive nature of model checkers. For each trace of the unmodified model that would be generated by Bandera, the modified model creates a trace in which each instance of the QuantifiedClass will be bound to var. At the state in which the binding is established the modified temporal formula will trigger the checking of P_var.

Note that when nested quantification is used the var_selected condition is defined such that it is true only when all of the bound variables in the quantifiers have been assigned a non-null value.