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

BoundedBuffer Class Reference

List of all members.

Public Methods

 BoundedBuffer (int b)
synchronized void add (Object o)
synchronized Object take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add (java.lang.Object o)
synchronized java lang Object take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add ()
synchronized void take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add (java.lang.Object o)
synchronized java lang Object take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add ()
synchronized void take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add (java.lang.Object o)
synchronized java lang Object take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add (java.lang.Object o)
synchronized java lang Object take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add (java.lang.Object o)
synchronized java lang Object take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add ()
synchronized void take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add (java.lang.Object o)
synchronized java lang Object take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add (java.lang.Object o)
synchronized java lang Object take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add (java.lang.Object o)
synchronized java lang Object take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add (java.lang.Object o)
synchronized java lang Object take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add (Object o)
synchronized Object take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add (java.lang.Object o)
synchronized java lang Object take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add (java.lang.Object o)
synchronized java lang Object take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add (java.lang.Object o)
synchronized java lang Object take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add (java.lang.Object o)
synchronized java lang Object take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add ()
synchronized void take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add (java.lang.Object o)
synchronized java lang Object take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add ()
synchronized void take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add (java.lang.Object o)
synchronized java lang Object take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add (java.lang.Object o)
synchronized java lang Object take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add (java.lang.Object o)
synchronized java lang Object take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add ()
synchronized void take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add (java.lang.Object o)
synchronized java lang Object take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add (java.lang.Object o)
synchronized java lang Object take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add (java.lang.Object o)
synchronized java lang Object take ()
synchronized boolean isEmpty ()
 BoundedBuffer (int b)
synchronized void add (java.lang.Object o)
synchronized java lang Object take ()
synchronized boolean isEmpty ()

Private Attributes

Object[] buffer
int bound
int head
int tail
java lang Object[] buffer
java lang Object[] buffer
java lang Object[] buffer
java lang Object[] buffer
java lang Object[] buffer
java lang Object[] buffer
java lang Object[] buffer
java lang Object[] buffer
java lang Object[] buffer
Object[] buffer
java lang Object[] buffer
java lang Object[] buffer
java lang Object[] buffer
java lang Object[] buffer
java lang Object[] buffer
java lang Object[] buffer
java lang Object[] buffer
java lang Object[] buffer
java lang Object[] buffer
java lang Object[] buffer
java lang Object[] buffer
java lang Object[] buffer

Detailed Description

@observable EXP Full(this): (head == tail); EXP TailRange(this): (tail >= 0 && tail < bound); EXP HeadRange(this): (head >= 0 && head < bound);

Definition at line 20 of file BanderaTutorial/BBuffer.java.

Constructor & Destructor Documentation

BoundedBuffer::BoundedBuffer (  int   b )  [inline]
 

@assert PRE PositiveBound: (b > 0);

Definition at line 28 of file BanderaTutorial/BBuffer.java.

BoundedBuffer::BoundedBuffer (  int   b )  [inline]
 

@assert PRE PositiveBound: (b > 0);

Definition at line 28 of file BoundedBuffer/BBuffer.java.

Member Function Documentation

synchronized void BoundedBuffer::add (  Object   o )  [inline]
 

@assert POST AddToEnd: (head == 0) ? buffer[bound-1]==o : buffer[head-1]==o; @observable INVOKE Call(this);

Definition at line 41 of file BoundedBuffer/BBuffer.java.

synchronized void BoundedBuffer::add (  Object   o )  [inline]
 

@assert POST AddToEnd: (head == 0) ? buffer[bound-1]==o : buffer[head-1]==o; @observable INVOKE Call(this);

Definition at line 41 of file BanderaTutorial/BBuffer.java.

synchronized boolean BoundedBuffer::isEmpty (    )  [inline]
 

@observable RETURN ReturnTrue(this): ($ret == true);

Definition at line 68 of file BoundedBuffer/BBuffer.java.

synchronized boolean BoundedBuffer::isEmpty (    )  [inline]
 

@observable RETURN ReturnTrue(this): ($ret == true);

Definition at line 68 of file BanderaTutorial/BBuffer.java.

Referenced by take().

synchronized Object BoundedBuffer::take (    )  [inline]
 

@observable RETURN Return(this);

Definition at line 54 of file BoundedBuffer/BBuffer.java.

synchronized Object BoundedBuffer::take (    )  [inline]
 

@observable RETURN Return(this);

Definition at line 54 of file BanderaTutorial/BBuffer.java.

The documentation for this class was generated from the following files:
Generated at Thu Feb 7 07:05:34 2002 for Bandera by doxygen1.2.10 written by Dimitri van Heesch, © 1997-2001