---

BoundedBuffer.java

class BoundedBuffer 
{
     java.lang.Object[] buffer;
     int tail;
     int head;
     int bound;
     
     public BoundedBuffer(int b)
     {
          Bandera.assert((b > 0) );
          this.bound = b;
          this.buffer = new java.lang.Object[this.bound];
          this.head = 0;
          this.tail = (this.bound - 1);
     }
     
     public synchronized void add (java.lang.Object o)
     {
          while (this.tail == this.head)
          {
               try {
                    this.wait();
               }
               catch (java.lang.InterruptedException ex) {
               }
          }
          this.buffer[this.head] = o;
          this.head = ((this.head + 1) % this.bound);
          this.notifyAll();
          Bandera.assert((this.buffer[(this.head - 1)] == o) );
     }
     
     public synchronized java.lang.Object take ()
     {
          while (this.isEmpty())
          {
               try {
                    this.wait();
               }
               catch (java.lang.InterruptedException ex) {
               }
          }
          this.tail = ((this.tail + 1) % this.bound);
          this.notifyAll();
          return $ret;
     }
     
     public synchronized boolean isEmpty ()
     {
          return (this.head == ((this.tail + 1) % this.bound));
     }
}

---