One of the chief difficulties in specifying properties of Java programs lies in naming the objects that constitute the state of the system. The majority of program state is heap allocated and is referenced through local thread variables by navigating chains of object references. We believe that, in general, one is interested in stating properties about all instances of a class or by distinguishing instances of a class by observing their state. One way to achieve this is to provide the ability to state properties for all instances of a class created during a program run.
The syntax for universal class instance quantification is given in Figure 19. BSL provides this through a mechanism that is independent of the specific checker used to reason about the property defined in the scope of the quantifier. This is achieved by customizing the model based on the quantifiers used and by embedding the property to be checked in a specification pattern that assures it will be checked only over the objects in the quantifier's domain.
For clarity, we describe the customization of the model in terms of a source program transformation rather than as a transformation on Bandera's intermediate program representation. This transformation requires the use of non-determinism in the model, which is not available in Java, so we introduce a static method Bandera.choose that is translated by Bandera to non-deterministic choice among its arguments in the model checker input. We also describe the embedding of a quantified LTL property; the approach is similar for other formalisms.