The words ``eventually become'' in the requirement suggest that the
property should be specified not as an assertion, but as temporal
property. Following the methodology of Figure 5.5.1,
we examine the code and see that the notion of full can be
expressed by a BSL EXP instance predicate on the variables head_
and tail_ of the BoundedBuffer class.
Specifically, the buffer is full when the head_ is equal to the
tail_. Thus, we add the following definition to the header of the
BoundedBuffer class.
/** * @observable * EXP Full: (head_ == tail_); */
Now we are ready to specify the temporal property that expresses
``whenever a buffer is full, eventually it will become non-full''.
Notice that this property as the same temporal structure as the
Pipeline shutdown property from the previous section:
``whenever the main method of the Pipeline class issues a stop call,
eventually the stage one thread will shutdown''.
Thus, we will use the same temporal pattern here, i.e., we use
response property with global scope.
Since will use the instance predicate above which refers to variables
in the BoundedBuffer class, we need to quantify over all
instances of BoundedBuffer.
The final version of the specification is as follows.
FullToNonFull: forall[b:BoundedBuffer].
{!Full(b)} responds to {Full(b)} globally