Main Page   Packages   Class Hierarchy   Alphabetical List   Compound List   File List   Compound Members  

BBuffer.java

00001 public class BBuffer {
00002    public static void main (String [] args) {
00003      BoundedBuffer b1 = new BoundedBuffer(3);
00004      BoundedBuffer b2 = new BoundedBuffer(3);
00005 
00006      b1.add(new Object());
00007      b1.add(new Object());
00008 
00009      (new InOut1(b1,b2)).start();
00010      (new InOut2(b2,b1)).start();
00011    }
00012 }
00013 
00014 /**
00015  * @observable
00016  *   EXP Full(this): (head == tail);
00017  *   EXP TailRange(this): (tail >= 0 && tail < bound);
00018  *   EXP HeadRange(this): (head >= 0 && head < bound);
00019  */
00020 class BoundedBuffer {
00021    Object [] buffer;
00022    int bound, head, tail;
00023 
00024    /**
00025     * @assert
00026     *   PRE PositiveBound: (b > 0);
00027     */
00028    public BoundedBuffer(int b) {
00029      bound = b;
00030      buffer = new Object[bound];
00031      head = 0;
00032      tail = bound-1;
00033    }
00034 
00035    /**
00036     * @assert
00037     *   POST AddToEnd: (head == 0) ? buffer[bound-1]==o : buffer[head-1]==o;
00038     * @observable
00039     *   INVOKE Call(this);
00040     */
00041    public synchronized void add(Object o) {
00042     while ( tail == head )
00043       try { wait(); } catch ( InterruptedException ex) {}
00044 
00045     buffer[head] = o;
00046     head = (head+1) % bound;
00047     notifyAll();
00048    }
00049 
00050    /**
00051     * @observable
00052     *   RETURN Return(this);
00053     */
00054    public synchronized Object take() {
00055      while ( isEmpty() )
00056        try { wait(); } catch ( InterruptedException ex) {}
00057 
00058      successTake:
00059      tail = (tail+1) % bound;
00060      notifyAll();
00061      return buffer[tail];
00062    }
00063 
00064    /**
00065     * @observable
00066     *   RETURN ReturnTrue(this): ($ret == true);
00067     */
00068    public synchronized boolean isEmpty() { return head == ((tail+1) % bound); }
00069 }
00070 
00071 class InOut1 extends Thread {
00072   BoundedBuffer in,out;
00073   public InOut1(BoundedBuffer ins, BoundedBuffer outs) {
00074     in = ins;
00075     out = outs;
00076   }
00077   public void run() {
00078     Object tmp;
00079     while(true) {
00080       tmp = in.take();
00081       System.out.println("Take 1");
00082       out.add(tmp);
00083       System.out.println("Put 1");
00084     }
00085   }
00086 }
00087 
00088 class InOut2 extends Thread {
00089   BoundedBuffer in,out;
00090   public InOut2(BoundedBuffer ins, BoundedBuffer outs) {
00091     in = ins;
00092     out = outs;
00093   }
00094   public void run() {
00095     Object tmp;
00096     while(true) {
00097       tmp = in.take();
00098       System.out.println("Take 2");
00099       out.add(tmp);
00100       System.out.println("Put 2");
00101     }
00102   }
00103 }

Generated at Thu Feb 7 06:40:39 2002 for Bandera by doxygen1.2.10 written by Dimitri van Heesch, © 1997-2001