While assertions provide a convenient way to write constraints on data at particular program points, they are not powerful enough to directly specify interesting temporal relationships between system actions. Since such temporal properties are often required of concurrent systems, model-checkers usually support a temporal property specification language based on, e.g., LTL or CTL. These temporal specification languages subsume assertions in the sense that any assertion (l,c), where l is a location and c a condition on the data at that location, can be encoded in a temporal property: along all paths, it must be true in every state s that if s's control point is l then c holds. However, model-checkers, such as Spin, provide support for assertions because they can be checked much more efficiently than general temporal properties. To take advantage of the potential for faster checks, BSL separates assertion and general temporal properties.
In this section, we describe BSL's temporal specification sublanguage. First, we introduce a system of predicates on program features including common control points such as method entry and exit, and both class and instance data. These predicates become the primitive propositions that one reasons about when writing temporal property specifications. We describe our extensible pattern-based system for constructing temporal specifications. Woven throughout both the predicates and the temporal patterns is a notion of object quantification that provides a mechanism for generating names of dynamically created objects.