The word ``always'' in requirement three suggests that the requirement
is a simple invariant property. Following the methodology of
Figure 5.5.1, we examine the code and see that
the notion of indices in range can be expressed by an
appropriate constraint on the BoundedBuffer instance variables
head_, tail_, and bound_. Thus, we define
the range notion as in instance predicate by inserting the following
declaration to the header of the
BoundedBuffer class.
/** * @observable * EXP IndexRange: (head_ >= 0 && tail_ >= 0 && head_ < bound_ && tail_ < bound_); */The tag
@observable indicates that a predicate for
a temporal property is being defined. The label EXP
is used to define a location insensitive predicate, i.e., a predicate that
only defines some constraint on data without mentioning a particular
control point. The predicate above is an instance predicate
(and thus must be quantified in the temporal property) because
it refers to instance variables in the BoundedBuffer class.
Typically, an invariant is defined using
EXP predicates since by the very nature of an invariant
the property should hold across multiple control points.
Now we can specify the temporal property that will use
IndexRange predicate. Positive invariants correspond to the
universal temporal pattern. Since the invariant is to hold through
the entire execution of the program, the scope of the property is
global. We also need to quantify the property for all instances of
the BoundedBuffer. The final version of the property expressed
in BSL is as follows:
IndexRange: forall[b:BoundedBuffer].
{IndexRange(b)} is universal globally;