There are several advantages to implementing support for quantification early in the process of extracting finite-state models from Java programs : checker independence and optimization.
The technique described above is applied to the internal representation of Java code prior to the generation of model checker input, e.g., Promela for Spin. Thus, quantified temporal specifications can be checked with any of the supported verifiers. Furthermore, since it is possible to generate Java from our internal representation, it is possible for Java model checkers, such as Java Pathfinder 2 from NASA's Ames Laboratory, to check quantified temporal specifications as long as they map the Bandera.choose method calls to non-deterministic choice in the underlying model.
The scopes in specification patterns define the end-points of regions in which the pattern should be checked. If those end-points do not occur, then the specification is vacuously true. For this reason, by performing object flow analyses [8] we can determine the set of objects that can possibly influence the satisfaction of scope delimiting predicates. This information can be used to restrict the set of objects over which a quantifier must range. Consider the specification
forall[s:SuperType].
{Pred(s)} is absent after {init.Return(s)}
in this case we need only calculate the set of instances
of SuperType for which the init method is
called. An upper approximation of this set
can by calculated in terms of the sub-types of SuperType
that can appear as the receiver object of an init invocation.
The code from step 3, described above, need only be added to those
sub-types; this may significantly reduce the cost of checking
the quantified property by reducing the number of values that
will be assigned to the bound variable, s.