BSL provides two kinds of predicates: location insensitive
predicates--predicates that are used for defining observables
regardless of program points, and location sensitive
predicates--predicates that are used for defining observables at
specific program points. For example, Section 5.6
gave a
declaration of a location insensitive predicate
EXP Full: (head == tail)
in the class BoundedBuffer header documentation.
This form of predicate, called an expression predicate, is
often used to define class invariants or to indicate distinguished
states (e.g., a full buffer) in class or instance data. Since
expression predicates do not refer to particular control points in
methods, they can only be defined in class header documentation.
In addition to categorizing predicates based on location sensitivity,
we also categorize predicates based on the kinds of fields or code to
which they refer. Static predicates are used to reason about
static fields (class variables) or program points of
static Java methods. Instance predicates are used to reason
about instance fields (memory cells that appear in each object of a
given class) or program points in Java virtual methods. For example,
the Full predicate is an instance predicate, because it refers
to instance data members of the BoundedBuffer class. The
static modifier is used in an expression predicate declaration
to indicate that it is a static predicate. When an instance predicate
is used in a specification, it must be passed a parameter to indicate
the instance to which the predicate applies. For example, the
FullToNonFull property of Figure 15
shows the Full
predicate being parameterized by the quantified variable b.