Source code properties to be checked are written in the Bandera Specification Language (BSL). BSL is based on a collection of field-tested temporal specification patterns [7] that allow users to write specifications in a stylized English format. These patterns essentially are parameterized macros that can be instantiated to one or more temporal logics such as LTL or CTL. Thus, this pattern system addresses the specification problem mentioned in the previous section by providing the user with temporal structures commonly used in specifications.
BSL specifications are parameterized by observables (predicates on program state) that are defined in Java source code using Javadoc comment notation. From a foundational standpoint, BSL specifications are instantiated to assertions and temporal logic formulas, and user-declared observables are the primitive propositions that can appear in those formulas. The property front-end of Figure 1 calls the Java front-end to extract all the observables declared in the given source program, it type checks the declared observables, and it instantiates the BSL specification to a particular temporal logic, and it translates the observables used in the input specification to the lower-level model representation. This last step addresses the representation gap issue of the specification problem by automatically translating properties described in terms of source-level features to the low-level optimized model representation.