Requirement five

For the final requirement Empty buffers must be added to before being taken from, there are three notions for which we need to define source code predicates: (1) the notion of empty buffer, (2) the event of adding an object to a buffer, and (3) the event of taking an object from a buffer.

The notion of empty buffer can be defined using the following instance predicate to code the test implemented in the isEmpty method.

/**
 * @observable
 *   EXP Empty: head_ == ((tail_+1) % bound_;
 */

The event of adding an object to a buffer can be defined by usin an INVOKE observable in the header of the add method.

  /**
    * @observable
    *   INVOKE Call;
    */

The event of removing an object from a buffer can be defined by usin a RETURN observable in the header of the take method.

  /**
    * @observable
    *   RETURN Return;
    */

To specify the temporal property, we will use the absence pattern with after/until scope. All of the predicates defined above are instance predicates on BoundedBuffer members, so we'll quantify over all BoundedBuffers.

  NoTakeWhileEmpty:
     forall[b:BoundedBuffer].
       {take.Return(b)} is absent
           after {Empty(b) until {add.Call(b)}