This study was presented by B. Möller at the 47th Meeting of IFIP WG 2.1 Algorithmic Languages and Calculi, Hong Kong, January 1995. It is part of an attempt at deductive design of an asynchronous bounded hardware queue.
The mathematical basis is the framework of ideal streams. A number of distributivity and monotonicity properties for the operators involved are proved. They are the basis for correct refinement of the specification into an implementation.
As predicative specification of a buffer of capacity n we use that
in all
finite prefixes of allowable streams the number of inputs may exceed
the
number of outputs by at most n. By the well-known decomposition
property
(which has a very simple algebraic proof here) one can decompose
any buffer
into a parallel composition of buffers of capacity 1. For this case
a
simple unfold/fold transformation and use of Arden's rule yield the
behaviour 
, where a and b are the actions of input
and
output, respectively. The approach is simpler and more algebraic than the
one in
[Olderog 91]. The study is concluded by a specification and calculation
of
a bounded queue which is specified as a bounded buffer which preserves
order and multiplicity of the values in the input.