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 are summarised in the following table:
2. Design
The design is based on the idea of a circular array. We will maintain two indices into this array, a bottom, and a top, to delimit the values that are of interest; this part of the array is the concrete representation of the bounded buffer.
For the design we need five components in the state schema:
• array: a sequence of values
• maxsize: the capacity of the buffer
• bot: the index of the first value stored
• top: the index of the last value stored
• size: the number of values stored
Although the circular array is modelled as a sequence, this sequence will be used in a way that reflects our design intentions:
===Array[X]==========================
When the buffer is full, we have size=maxsize; when the buffer is empty we have size=0. In either of these two extremes, it is the case that
top+1 mod maxsize = bot
As in the specification, we will insist that the capacity of the buffer cannot be changed after instalation:
===UpdateArray[X]=====================
In what follows, we need a shift operator on sequences, denoted by . ≪ . and defined by the schema:
===[X]=============================
Now we can define the retrieve relation. If we cut the circular buffer immediately below the bot mark, and then strainghten it out, we will find that the first size elements are the same as those in the abstract buffer. If we shift the circular buffer so that bot occurs at position 1, and trim away the waste, then we have the abstract buffer. The retrieve relation is defined by the schema:
===RetrieveBuffer[X]===================
The succesful part of the input operation may be calculated as:
===ArrayIn0 [X]======================
In the predicate part of this schema the expression #((1..size) ⊳ ((bot - 1) ≪ array ))
appears twice. It can be proved that the value of this expression is equal to the number of elements in the buffer, that is size. After simplifying the second predicate of the schema, we arrive at the following concrete operation schema that describes the effect of a successful input:
===ArrayIn0 [X]======================
The error case for concrete operation is easily calculated:
===ArrayInError[X]===============
The total form of the input operation is then described by:
ArrayInError[X] = = (ArrayIn0 [X] ∧ Success) ∨ ArrayInError[X]
A similar calculation yields the concrete form of the output operation:
===ArrayOut0[X]===================
After simplifications, the operation schema that describes the concrete output operation becomes:
===ArrayOut0[X]================
The error case is given by the schema:
===ArrayOutError[X]==============
The robust version of the concrete output operation is then
ArrayOut[X] = = ArrayOut0 [X] ∧ Success ∨ ArrayOutError[X]
3. Implementation
Our implementation of the design will be parameterised by the maximum size of the buffer. The global declarations for our bounded buffer module will be:
Var ibuffer : array[1..maxsize] of X;
bot, top : 1..maxsize;
size : 0..maxsize;
and size mod maxsize = (top-bot+1) mod maxsize.
We will begin with the concrete input operation:
IBuffer[X] = = Array’[X] : [true, ArrayIn0 [X] ∧ Success ∨ ArrayInError[X] ]
The derivation of code is quite simple. First, IBuffer[X] is refined to:
IF
size<maxsize → Array’[X] : [size<maxsize, ArrayIn0 [X] ∧ Success ]
size=maxsize → Array’[X] : [size=maxsize, ArrayInError[X]]
FI
We refine the first alternative (strenghtening the postcondition):
IF
size<maxsize → Array’[X] : [size<maxsize, post1
size=maxsize → Array’[X] : [size=maxsize, ArrayInError[X]]
FI
where
post1 ::= (size’=size+1) ∧ (bot’=bot) ∧ (top’=1+ top mod maxsize) ∧
(ibuffer’ = ibuffer ⊕+{top’-x?}) ∧ (report!=ok)
and then the the second alternative (also strenghtening the postcondition):
IF
size<maxsize → Array’[X] : [size<maxsize, post1]
size=maxsize → Array’[X] : [size=maxsize, report!=full]
FI
At last, by assignement law, we arrive at:
Procedure BufferIn[X] (val x:X; res report!:Report);
IF
size<maxsize → size := size+1;
top:=(top mod maxsize) + 1;
ibuffer[top]:=x;
report!=ok
□ size=maxsize → report!:=full
FI
The following specification statement corresponds closely to the concrete output operation
IBufferOut[X] ::= Array’[X] : [true, ArrayOut0 [X] ∧ Success ∨ ArrayOutError[X] ]
which may be refined to (alternative law):
IF
Size≠0 → Array’[X] : [size≠0, ArrayOut0[X] ∧ Success ]
Size=0 → Array’[X] : [size=0, ArrayOutError[X]]
FI
We refine the first alternative (strenghtening the postcondition):
IF
size<maxsize → Array’[X] : [size≠0, post3]
size=maxsize → Array’[X] : [size=0, ArrayOutError[X]]
FI
where
post3 ::= (size’=size-1) ∧ (bot’=bot mod maxsize + 1) ∧
(array’ = array) ∧ (report!=ok)
By assignement law, it is refined to:
IF
size<maxsize → size’:=size-1; bot:=(bot mod maxsize)+ 1; report!=ok
size=maxsize → Array’[X] : [size=0, ArrayOutError[X]]
FI
and then the the second alternative (also strenghtening the postcondition):
IF
size<maxsize → size’:=size-1; bot:=(bot mod maxsize)+ 1; report!=ok
size=maxsize → Array’[X] : [size=0, report!=empty]
FI
and, by assignement law, we arrive at:
Procedure BufferOut (res report!:Report);
IF
size ≠0→ size := size-1;
bot:=(bot mod maxsize) + 1;
report!=ok
size= 0 → size=0;
report!:=full
FI
Similarly, we may derive a procedure that accepts a single value and resets the buffer to hold just that value:
Procedure ResetBuffer[X] (val x:X);
Bot, top, size, ibuffer[1]:=1, 1, 1, x
A suitable initialisation for the buffer module is described by the following assignement:
Initially bot, top, size := 1, maxsize, 0