Figure 18: BSL predicate definition syntax
Figure 18 gives the syntax of BSL predicate
definitions. Sets of predicates are defined using the Javadoc tag
@observable in the header documentation for classes or methods.
Each predicate set defined by an @observable tag can be given
an optional name, and this name along with the name for each predicate
in the set, is used to uniquely identify the predicate so that it can
be referred to in a temporal property specification. If the set name
is omitted, the fully qualified name of the corresponding class or
method is used as the name for the predicate set. The optional name is
followed by zero or more Java newline comments.
Besides expression predicates as illustrated above, BSL supports invocation predicates, location predicates, and return predicates, which are all location sensitive predicates that are defined in method header documentation. These location sensitive predicates are static if they are defined for static methods.
INVOKE <predicate-name> [: <exp>]? is true when control is at
the first executable statement in the corresponding method and
<exp> is true; absence of <exp> defaults to true. For instance
INVOKE predicates, an additional constraint applies: the supplied
object parameter must match the receiver object (i.e., the
object upon which the method was invoked). For example,
in the NoTakeWhileEmpty property of Figure 15,
the instance INVOKE predicate add.Call holds
only when the add method is invoked on the object referenced by
the quantified variable b.
The semantics of
LOCATION '[' <label> ']' <predicate-name> [:<exp>]?
is similar to that of the invoke predicate, except that the
relevant control point is the Java statement labeled by <label>
in the corresponding method.
RETURN <predicate-name> [:<exp>]? is similar to an
invoke predicate, except that the relevant
control points are the points immediately after any of the
corresponding method's return statements or after the last
statement in the method if it has no return statement. The expression
<exp> can refer to the return value of the method using the
Bandera reserved identifier $ret. For example, in the
NoTakeWhileEmpty property of Figure 15, the
instance RETURN predicate take.Return holds iff the
take method was invoked on the object referenced by the
quantified variable b and control is immediately after
the return statement of take.
The Java expressions that are supported in <exp> are Java expressions
that are guaranteed to have no side-effects. Currently we
restrict Java expressions to exclude
assignments, array or object creations, and method invocations to
assure side-effect freedom.
There are various other well-formedness conditions associated with variable scoping that we will not discuss in detail here. For example, a return predicate cannot refer to local variables of the method since there might be several return statements for the method with each having a different set of visible local variables.