---

BBuffer.java

public class BBuffer {
   public static void main (String [] args) {
     BoundedBuffer b1 = new BoundedBuffer(3);
     BoundedBuffer b2 = new BoundedBuffer(3);

     b1.add(new Object());
     b1.add(new Object());

     (new InOut1(b1,b2)).start();
     (new InOut2(b2,b1)).start();
   }
}

/**
 * @observable
 *   EXP Full(this): (head == tail);
 *   EXP TailRange(this): (tail >= 0 && tail < bound);
 *   EXP HeadRange(this): (head >= 0 && head < bound);
 */
class BoundedBuffer {
   Object [] buffer;
   int bound, head, tail;

   /**
    * @assert
    *   PRE PositiveBound: (b > 0);
    */
   public BoundedBuffer(int b) {
     bound = b;
     buffer = new Object[bound];
     head = 0;
     tail = bound-1;
   }

   /**
    * @assert
    *   POST AddToEnd: (head == 0) ? buffer[bound-1]==o : buffer[head-1]==o;
    * @observable
    *   INVOKE Call(this);
    */
   public synchronized void add(Object o) {
    while ( tail == head )
      try { wait(); } catch ( InterruptedException ex) {}

    buffer[head] = o;
    head = (head+1) % bound;
    notifyAll();
   }

   /**
    * @observable
    *   RETURN Return(this);
    */
   public synchronized Object take() {
     while ( isEmpty() )
       try { wait(); } catch ( InterruptedException ex) {}

     successTake:
     tail = (tail+1) % bound;
     notifyAll();
     return buffer[tail];
   }

   /**
    * @observable
    *   RETURN ReturnTrue(this): ($ret == true);
    */
   public synchronized boolean isEmpty() { return head == ((tail+1) % bound); }
}

class InOut1 extends Thread {
  BoundedBuffer in,out;
  public InOut1(BoundedBuffer ins, BoundedBuffer outs) {
    in = ins;
    out = outs;
  }
  public void run() {
    Object tmp;
    while(true) {
      tmp = in.take();
      System.out.println("Take 1");
      out.add(tmp);
      System.out.println("Put 1");
    }
  }
}

class InOut2 extends Thread {
  BoundedBuffer in,out;
  public InOut2(BoundedBuffer ins, BoundedBuffer outs) {
    in = ins;
    out = outs;
  }
  public void run() {
    Object tmp;
    while(true) {
      tmp = in.take();
      System.out.println("Take 2");
      out.add(tmp);
      System.out.println("Put 2");
    }
  }
}

---