Bounded Buffer Module

A Bounded Buffer is a data store that may hold a finite number of values. It behaves as a first-in first-out queue: values leave in order in which they arrive. We will develop a programming language implementation of a bounded buffer with three operations:

• BufferInit - an initialisation

• BufferIn, providing input to the buffer

• BufferOut, accepting output from the buffer.

We must specify these operations, design , and implement them.

1. Specification

The state of a bounded buffer will include three components:

• buffer: a sequences of values

• size: the number of values present

• maxsize: an indication of the buffer’s capacity.

        The sequence buffer, and the state itself, will use a generic parameter X to refer to the type of values to be stored:

        ===Buffer[X]=================

        At initialization, the bounded buffer is empty: buffer is equal to the empty sequence and size is zero:

        ===BufferInit[X]==============

        The capacity of the buffer cannot be changed after instantiation; this fact is recorded as an invariant in the following schema:

        ===UpdateBuffer[X]============

        If the buffer is not full, an item may be inserted:

===BufferIn0 [X]==============

The new value is appended to the end of sequence buffer.

        Extracting an item is possible only if the buffer is not empty; the value obtained is the one at the head of buffer:

===BufferOut0 [X]=============

These schemas represent partial operations: they describe the effect of a succesful insertion and a succesful extraction, respectively.

        When the operations are not possible, some messages must be produced. We introduce the type

                Report  ::=  ok | full | empty

Join now!

The message ok will be used to indicate a favorable outcome to an operation,  full will be used to indicate that the buffer is full, and empty will be used to indicate that the buffer is empty.

        We include a succesful report defined by the schema:

===Success==================

or one of the error reports:

===BufferInError[X]============

===BufferOutError[X]===========

As usual, ΞBuffer[X] indicates that the state of the buffer is unchanged by this operation.

We may define total versions of the input and output operations:

BufferIn[X] = =   ( BufferIn0 Success  BufferInError[X] )

BufferOut[X]  =  (BufferOut0 Success  BufferOutError[X] )

The preconditions associated with these operations ...

This is a preview of the whole essay