In this section we will look at another multi-threaded JAVA program and use it to further illustrate construction of temporal specifications written in BSL. We'll start with a program that omits the Javadoc declaration of predicates and assertions, and you'll add appropriate declarations as an exercise. Once you've made these additions to the source code, we'll step through the definition of a few of the corresponding sessions and leave the remaining ones as exercises.
IncompleteBoundedBuffer.java
shows the program that we consider: it
implements a simple bounded buffer (in the BoundedBuffer class)
and contains several other auxiliary driver classes used to exercise
the behavior of the buffer.
The BoundedBuffer class has two methods used for adding and removing
elements from the buffer. You can add to the buffer if the buffer is not full
and if you have a lock of the BoundedBuffer that guarantees an
exclusive access to the buffer. If the buffer is not empty and you have
access to the buffer, you can take an element out of the buffer.
The BoundedBuffer has 4 fields: buffer_ represented by an array
of Elements, bound_, head_, and tail_ represented
by an int. The bound_ variable represents the number of slots
in the buffer_. The head_ variable points to the
next available slot in the buffer, and tail_ points to the last
available slot.
The main driver class is called IncompleteBoundedBuffer because
we have omitted the various BSL predicate definitions for the
properties that we will check later. After you have inserted the
definitions into your file, you can double check your work by looking
in the
CompleteBoundedBuffer.java
file in your tutorial
examples directory - that file contains code that is annotated with
the complete BSL definitions.
The driver creates two BoundedBuffers and two
threads called InOut1 and InOut2 that work with the
buffers. Thread InOut1 constantly takes an element out of the
first buffer and puts in into the second buffer. Thread InOut2
takes an element out of the second buffer and puts it into the first
one.